Formalizing Gröbner Basis Theory in Lean

Junyu Guo, Hao Shen, Junqi Liu +1

We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the…