Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

First steps towards Computational Polynomials in Lean

James Harold Davenport

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.

First steps towards Computational Polynomials 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.
Paper Structure (17 sections, 1 equation, 3 figures)

This paper contains 17 sections, 1 equation, 3 figures.

Table of Contents

  1. State of Lean
  2. Existing support
  3. Why both?
  4. A curious case
  5. Representations of Polynomials
  6. A preliminary choice
  7. Geobuckets
  8. An improvement
  9. Related work
  10. Choices of Multivariate Polynomial Representations
  11. Addition of Sparse polynomials
  12. Polynomial Multiplication
  13. Polynomial Verification
  14. A specialist input mechanism?
  15. Johnson1974, as described in MonaganPearce2009b
  16. ...and 2 more sections

Figures (3)

  • Figure 1: Lean addition
  • Figure 2: Definition of a multivariate polynomial
  • Figure 3: Sorted addition of multivariate polynomials