First steps towards Computational Polynomials in Lean
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916393441558528 |
|---|---|
| author | Davenport, James Harold |
| author_facet | Davenport, James Harold |
| contents | The proof assistant Lean has support for abstract polynomials, but this is not necessarily the same as support for computations with polynomials. Lean is also a functional programming language, so it should be possible to implement computational polynomials in Lean. It turns out not to be as easy as the naive author thought. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_04564 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | First steps towards Computational Polynomials in Lean Davenport, James Harold Symbolic Computation 68W30 G.4 The proof assistant Lean has support for abstract polynomials, but this is not necessarily the same as support for computations with polynomials. Lean is also a functional programming language, so it should be possible to implement computational polynomials in Lean. It turns out not to be as easy as the naive author thought. |
| title | First steps towards Computational Polynomials in Lean |
| topic | Symbolic Computation 68W30 G.4 |
| url | https://arxiv.org/abs/2408.04564 |