Lean and Computer Algebra

Mathlib defines polynomials, ideals, and Gröbner bases abstractly, as objects satisfying certain algebraic properties. A computer algebra system needs executable algorithms that actually compute a GCD, a normal form, or a Gröbner basis, and, ideally, a proof that the algorithm meets its abstract specification.

This gap between “Lean can state what a Gröbner basis is” and “Lean can compute one, and prove the computation correct” is exactly where formal verification meets computer algebra. As Davenport (2024) puts it, Lean’s support for abstract polynomials is “not necessarily the same as support for computations with polynomials” — closing that gap is harder than it looks.

Why it matters

Certified computer algebra. A computation whose correctness is a Lean theorem, not just a test suite, is immune to an entire class of implementation bugs. This matters most for the primitives (GCD, factorization, Gröbner bases) that everything else in a CAS is built on.
Executable Mathlib. Mathlib’s Gröbner basis theory (Buchberger’s criterion, existence/uniqueness of reduced Gröbner bases) is stated for arbitrarily many variables, which is elegant for proofs but not obviously executable — connecting the finite, computable case to the general theorem is itself a nontrivial formalization task.
A concrete target for #eval/native_decide. Lean can already run some polynomial computations; the interesting question is how far this reaches (efficiency, generality) before it needs proof-carrying certificates instead of direct execution.

Targets

Polynomial GCD. Implement a computable GCD for univariate polynomials over a field in Lean, and prove it agrees with Mathlib’s abstract gcd.

Buchberger’s algorithm. Implement Buchberger’s algorithm for a small multivariate polynomial ring and connect it to Mathlib’s existence theorem for reduced Gröbner bases (following Guo–Shen–Liu–Zhi, 2026).

Reflection-style certification. Investigate the “compute then verify” pattern used elsewhere in Lean/Coq: run an untrusted fast algorithm, then check its output against a slower, formally verified specification.

Goal

Implement one executable computer algebra primitive (polynomial GCD or a small Gröbner basis computation) in Lean 4, connect it to the corresponding Mathlib abstraction, and prove the connection.

Milestones

ID	Title
M1	Lean 4 + Mathlib setup; survey polynomial API
M2	Executable algorithm implemented (untrusted)
M3	Correctness proof connecting it to Mathlib
M4	Write-up + clean Lean file

Tasks

ID	Title	Status
T1	Learn Lean 4 + Mathlib’s polynomial/ideal API	todo
T2	Implement the executable algorithm	todo
T3	Prove correctness against Mathlib’s abstraction	todo
T4	Clean proof + write-up	todo

Deliverables

Self-contained Lean 4 file with an executable algorithm and a proof it matches Mathlib’s abstract specification
Short write-up on what made the algorithm hard to make both executable and verified (4–6 pages)

Resources

References

J. H. Davenport. First Steps Towards Computational Polynomials in Lean. SYNASC 2024, IEEE. DOI 10.1109/synasc65383.2024.00019 · arXiv:2408.04564
J. Guo, H. Shen, J. Liu, and L. Zhi. Formalizing Gröbner Basis Theory in Lean. arXiv:2602.12772, 2026. arxiv.org/abs/2602.12772

← All topics