First steps towards Computational Polynomials in Lean
arXiv:2408.04564
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.
Revised version to appear in Proc. SYNASC 2024