Reservoir

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 term
• MonomialOrder.sPolynomial: S-polynomial
• MonomialOrder.IsRemainder
• MonomialOrder.IsGroebnerBasis

Main Statements

Given a monomial order, a field , and an index set , we will show the following properties about :

• MonomialOrder.exists_groebner_basis: if the is finite, then each ideal has its Gröbner basis.
• MonomialOrder.groebner_basis_isRemainder_zero_iff_mem_span (WIP): given a Gröbner basis of an ideal , a polynomial , and a remainder of on division by , then if and only if .
• MonomialOrder.is_groebner_basis_iff: given an ideal and 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: if is a Gröbner basis of , then .
• MonomialOrder.buchberger_criterion: a finite set is 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:

• 📘 Project Homepage

• 📐 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