search

johoelzl / mason-stother

Lean formalization of the Mason-Stother theorem
0 stars 1 forks source link

Defining polynomials #1

Open JWageM opened 6 years ago

JWageM commented 6 years ago

How to define the type polynomial?

JWageM commented 6 years ago

Current libraries: Lean 0.3: https://github.com/leanprover/mathlib <- Polynomials not present. Lean 0.2: https://github.com/leanprover/lean2 polynomials not pressent, only a C++ file on them: https://github.com/leanprover/lean/blob/master/src/util/polynomial/polynomial.h

Possible definition: https://github.com/pj0y1/polynom is this usable? It seemed to advanced for me.

johoelzl commented 6 years ago

The C++ file in Lean 2 is an implementation to compute with polynomials, it is totally unrelated to a formal proof.

I didn't know about the work by pj0y1, it seams to be written in Lean 2. And the formalization is about concrete functions, instead of introducing polynomials as formal objects. For Mason-Stother it is important to have a concrete representation of polynomials to manipulate them, e.g. compute the derivative.