First steps towards Computational Polynomials in Lean

TL;DR

This paper explores the challenges of implementing computational polynomials in the Lean proof assistant, highlighting the gap between abstract support and actual computational capabilities.

Contribution

It investigates the difficulties in developing computational polynomials within Lean, providing initial insights into bridging the gap between theory and computation.

Findings

Identifies challenges in implementing computational polynomials in Lean

Highlights differences between abstract polynomial support and computational implementation

Provides initial steps towards computational polynomial support in Lean

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.