Groebner

The goal of this project is formalization of Gröbner basis theory in the Lean 4 theorem prover, establishing the mathematical infrastructure required for computational algebra in Lean. Based on it, we aim to bridge the gap between Lean and some computational algebra problems, such as solving systems of multivariate polynomial equations, ideal membership problems, and so on.

This project is still work in process. There are some errors and out-of-date information on our documents and maybe even unproved statements. Any fix and suggestions will be welcomed.

Introduction

Files

• Groebner/MonomialOrderEmbedding.lean: embedding between monomial orders;
• Groebner/MonomialOrder.lean: lemmas about monomial order and withBotDegree;
• Groebner/Remainder.lean: remainder;
• Groebner/Groebner.lean: Groebner basis;
• Groebner/Reduced.lean: reduced Gröbner basis;
• archive: archived version of the source code before updating to a new version of mathlib with some of our formalization merged.

Definitions

• MonomialOrder.leadingTerm: leading term
• MonomialOrder.sPolynomial: S-polynomial
• MonomialOrder.IsRemainder: remainder
• MonomialOrder.IsGroebnerBasis: Gröbner basis
• MonomialOrder.IsGroebnerBasis.IsMinimal: minimal Gröbner basis
• MonomialOrder.IsGroebnerBasis.IsReduced: reduced Gröbner basis

Main Statements

Given a monomial order, a field $k$, and an index set $\sigma$, we will show the following properties about $k[x_i:i\in \sigma]$:

• MonomialOrder.IsGroebnerBasis.exists_isGroebnerBasis: if the $\sigma$ is finite, then each ideal $I \subseteq k[x_i: i\in \sigma]$ has its Gröbner basis.
• MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal: given a Gröbner basis $G$ of an ideal $I\subseteq k[x_i: i\in \sigma]$, a polynomial $p\in k[x_i: i\in \sigma]$, and a remainder $r$ of $p$ on division by $G$, then $r = 0$ if and only if $p\in I$.
• MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero: given an ideal $I\subseteq k[x_i:i\in\sigma]$ and a set $G\subseteq k[x_i:i\in\sigma]$, then $G$ is a Gröbner basis of $I$ if and only if $G \subseteq I$ and $0$ is a remainder of each $p\in I$ on division by $G$.
• MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder: remainder of any polynomial on division by Gröbner basis is unique.
• MonomialOrder.IsGroebnerBasis.ideal_eq_span: if $G$ is a Gröbner basis of $I\subseteq k[x_i:i\in\sigma]$, then $I=\langle G\rangle$.
• MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero: (Buchberger's criterion) a set $G\subseteq k[x_i:i\in\sigma]$ is Gröbner basis of $\langle G\rangle$, if and only if $0$ is the remainder of the S-polynomial of each two elements in $G$ on division by $G$.
• MonomialOrder.IsGroebnerBasis.IsReduced.uniqueExists_of_isGroebnerBasis: unique existence of reduced Groebner basis.

Project Resources

We maintain a set of web-based resources to track and explore the formalization effort:

• 📘 Project Homepage

• 📐 Formalization Dependency Graph A detailed list of definitions, lemmas, and theorems, including their proof status and logical dependencies.

• 🔗 Dependency Graph A visual representation of the dependency structure of the formalized components.

These tools help us manage development, track formalization progress, and guide future contributors.

Build

To use this project, you'll need to have Lean 4 and its package manager lake installed. If you don’t already have Lean 4 set up, follow the Lean 4 installation instructions.

Once Lean is installed, you can clone this repository and build the project:

git https://github.com/WuProver/groebner_proj.git
cd groebner_proj
lake exe cache get
lake build

The dependency graph can be generated as following:

pip install https://github.com/WuProver/plastexdepgraph/archive/refs/heads/settitle.zip leanblueprint
./generate-content.sh
leanblueprint pdf
leanblueprint web

Reference

This project draws heavily from Ideals, Varieties, and Algorithms by David A. Cox, John Little, Donal O’Shea.

And some theorems are from Gröbner Bases for the Polynomial Ring with Infinite Variables and Their Applications by Kei-ichiro Iima and Yuji Yoshino.