This repository contains a Lean 4 formalization of Buchberger's Algorithm for computing Gröbner bases in polynomial rings. Gröbner bases, introduced by Bruno Buchberger in 1965, are a fundamental tool in computational algebra, providing a systematic way to solve polynomial systems.
This project is based on Lean 4 and Mathlib, and aims to rigorously formalize polynomial ideal theory, closely following standard references such as Ideals, Varieties, and Algorithms [CLO1997] and Gröbner Bases [BW1993].
- Blueprint of the proof: 📚 Buchberger Blueprint
- Documentation of the methods: 📜 Lean API Docs
- GitHub Repository: 🔗 GitHub
- Discussion on Zulip: 💬 Zulip Chat
Buchberger/- Lean 4 source files- Contains Lean formalizations (e.g.,
MonomialIdeal.lean,GroebnerBases.lean)
- Contains Lean formalizations (e.g.,
blueprint/- Lean Blueprint documentationsrc/- LaTeX sources for the Blueprintchapter/- Individual chapters in LaTeXmacros/- Common and format-specific macros (common.tex,web.tex,print.tex)content.tex- Main Blueprint content file
web/- HTML output of the Blueprint (afterleanblueprint web)print/- PDF output of the Blueprint (afterleanblueprint pdf)
home_page/- Jekyll-based GitHub Pages websitelakefile.toml- Lean 4 package configurationREADME.md- This file!.github/workflows/- Continuous integration (CI) for Lean & Blueprint
To compile the Lean 4 code, ensure you have Lean installed.
Follow the Lean installation guide.
To generate the Blueprint (formalization document) and web version, run:
leanblueprint webTo generate the PDF version, run:
leanblueprint pdf
The compiled PDF document will be located at:
blueprint/print/print.pdf
[CLO1997]: https://www.springer.com/gp/book/9780387946801
Cox, Little, and O'Shea, Ideals, Varieties, and Algorithms, Springer, 1997.
[BW1993]: https://www.cambridge.org/core/books/grobner-bases/2A360FC17BB715C2C99402D16A204BD6
Becker and Weispfenning, Gröbner Bases, Cambridge University Press, 1993.