Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing Gröbner Basis Theory in Lean

Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi

TL;DR

This work presents a Lean 4 formalization of Gröbner basis theory built on Mathlib, extending to polynomial rings indexed by arbitrary types and to infinite-variable settings. It introduces a degree-with-bottom construction to fix zero-polynomial ambiguities, formalizes polynomial division and remainder, and develops the full Gröbner basis apparatus including Buchberger's criterion and reduced bases, with both finite and infinite-variable results. A key contribution is the finite–infinite variable bridge, using monomial-order embeddings and filter-based liminf constructions to characterize infinite Gröbner bases via finite reductions. The resulting framework provides a robust, reusable foundation for certified algebraic geometry and future formalizations in Lean, enabling reliable verification of polynomial-algebra algorithms in both finite and infinite contexts.

Abstract

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.

Formalizing Gröbner Basis Theory in Lean

TL;DR

This work presents a Lean 4 formalization of Gröbner basis theory built on Mathlib, extending to polynomial rings indexed by arbitrary types and to infinite-variable settings. It introduces a degree-with-bottom construction to fix zero-polynomial ambiguities, formalizes polynomial division and remainder, and develops the full Gröbner basis apparatus including Buchberger's criterion and reduced bases, with both finite and infinite-variable results. A key contribution is the finite–infinite variable bridge, using monomial-order embeddings and filter-based liminf constructions to characterize infinite Gröbner bases via finite reductions. The resulting framework provides a robust, reusable foundation for certified algebraic geometry and future formalizations in Lean, enabling reliable verification of polynomial-algebra algorithms in both finite and infinite contexts.

Abstract

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.
Paper Structure (9 sections, 14 theorems, 15 equations, 1 figure)

This paper contains 9 sections, 14 theorems, 15 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Formalizing Gröbner Basis Theory in Lean
  4. Degree with Bottom Element
  5. Polynomial Division and Remainder
  6. Gröbner Basis
  7. Buchberger Criteria
  8. Reduced Gröbner Basis
  9. Finite Characterization of Infinite Gröbner Bases

Key Result

Theorem 1

Fix a monomial order. For any polynomial $f \in k[x_i]_{i\in\sigma}$ and any ordered tuple of polynomials $B = (f_1, \ldots, f_s)$ in $k[x_i]_{i\in\sigma}$, there exist polynomials $a_1, \ldots, a_s \in k[x_i]_{i\in\sigma}$ and a polynomial $r \in k[x_i]_{i\in\sigma}$ such that and $r$ is a remainder of $f$ with respect to the set $\{f_1, \ldots, f_s\}$ in the sense of Definition isremainder.

Figures (1)

  • Figure 1: Structure of the formalization of Gröbner basis

Theorems & Definitions (25)

  • Definition 1: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=MonomialOrder#src
  • Definition 2: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=MonomialOrder.lex#src
  • Definition 3: https://wuprover.github.io/groebner_proj/docs/find/?pattern=MonomialOrder.leadingTerm#src
  • Definition 4: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=MonomialOrder.leadingCoeff#src
  • Definition 5: Leading Monomial
  • Definition 6: https://wuprover.github.io/groebner_proj/docs/find/?pattern=MonomialOrder.IsRemainder#src
  • Theorem 1: https://wuprover.github.io/groebner_proj/docs/find/?pattern=MonomialOrder.IsRemainder.exists_isRemainder#src
  • Definition 7: https://wuprover.github.io/groebner_proj/docs/find/?pattern=MonomialOrder.IsGroebnerBasis#src
  • Theorem 2
  • Theorem 3
  • ...and 15 more