Formalizing Gröbner Basis Theory in Lean
This work formalizes a key algebraic tool for theorem proving and computational algebra, but it is incremental as it builds on existing Mathlib infrastructure.
The authors tackled the formalization of Gröbner basis theory in Lean 4, covering core foundations like Buchberger's criterion and enabling treatment for polynomial rings with infinitely many variables, resulting in a development that connects finite and infinite settings through monomial-order embeddings and filter-based limits.
We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the core foundations of Gröbner basis theory, including polynomial division with remainder, Buchberger's criterion, and the existence and uniqueness of reduced Gröbner bases. We develop the theory uniformly for polynomial rings indexed by arbitrary types, enabling the treatment of Gröbner bases in rings with infinitely many variables. Furthermore, we connect the finite and infinite settings by showing that infinite-variable reduced Gröbner bases can be characterized via reduced Gröbner bases on finite-variable subrings through monomial-order embeddings and filter-based limit constructions.