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.

Open in GitHub Codespaces

Open in Gitpod

Introduction

Definitions

Main Statements

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

Project Resources

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

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