First steps towards Computational Polynomials in Lean
Symbolic Computation
2024-09-17 v2
Abstract
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.
Cite
@article{arxiv.2408.04564,
title = {First steps towards Computational Polynomials in Lean},
author = {James Harold Davenport},
journal= {arXiv preprint arXiv:2408.04564},
year = {2024}
}
Comments
Revised version to appear in Proc. SYNASC 2024