Buchberger Algorithm Formalization

This site accompanies a Lean 4 formalization of relation-theoretic polynomial reduction, Groebner basis criteria, and an abstract Buchberger procedure.

The Lean source is maintained in a public Mathlib fork and fixed at commit 4868fec773dcba035d283904f8b118511cc83d73.

Links

• Generated API documentation
• Artifact and reproducibility instructions
• Canonical Lean source
• Development branch
• Archived prototype and Blueprint

The arXiv link will be added when the first manuscript version is deposited.