{"id":"arxiv/2602.12772","url":"https://arxiv.org/abs/2602.12772","tags":["math.AC","cs.LO","math.RA"],"score":0,"title":"Formalizing Gröbner Basis Theory in Lean","domain":"math.AC","source":"arxiv","authors":["Junyu Guo","Hao Shen","Junqi Liu","Lihong Zhi"],"reviews":0,"subject":"math.AC","summary":"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 core foundations of Gröbner basis theory, including polynomial division with remainder, Buchberger's criterion, and the existence and uniqueness of reduced Gröbner bases. We develop the theory uniformly for polynomial rings indexed by arbitrary types, enabling the treatment of Gröbner bases in rings with infinitely many variables. Furthermore, we connect the finite and infinite settings by showing that…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-02-13","reactions":{}}