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
Definitions
MonomialOrder.leadingTerm
: leading termMonomialOrder.sPolynomial
: S-polynomialMonomialOrder.IsRemainder
MonomialOrder.IsGroebnerBasis
Main Statements
Given a monomial order, a field
MonomialOrder.exists_groebner_basis
: if theis finite, then each ideal has its Gröbner basis. MonomialOrder.groebner_basis_isRemainder_zero_iff_mem_span
(WIP): given a Gröbner basisof an ideal , a polynomial , and a remainder of on division by , then if and only if . MonomialOrder.is_groebner_basis_iff
: given an idealand a finite set , then is a Gröbner basis of if and only if and is a remainder of each on division by . MonomialOrder.span_groebner_basis
: ifis a Gröbner basis of , then . MonomialOrder.buchberger_criterion
(WIP): a finite setis Gröbner basis of , if and only if is the remainder of the S-polynomial of each two elements in on division by .
Project Resources
We maintain a set of web-based resources to track and explore the formalization effort:
-
📐 Formalization Blueprint 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 blueprint 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 the following reference: Ideals, Varieties, and Algorithms