Formalizing Gr\"obner Basis Theory in Lean

TL;DR

This paper formalizes the core aspects of Gr"obner basis theory within Lean 4, extending the framework to infinite-variable polynomial rings and connecting finite and infinite cases through advanced constructions.

Contribution

It provides a comprehensive formalization of Gr"obner basis theory in Lean 4, including infinite-variable cases and the relationship between finite and infinite settings.

Findings

Formalization includes polynomial division, Buchberger's criterion, and reduced Gr"obner bases.

Extends theory to polynomial rings with infinitely many variables.

Connects finite and infinite-variable Gr"obner bases via monomial-order embeddings.

Abstract

We present a formalization of Gr\"obner 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\"obner basis theory, including polynomial division with remainder, Buchberger's criterion, and the existence and uniqueness of reduced Gr\"obner bases. We develop the theory uniformly for polynomial rings indexed by arbitrary types, enabling the treatment of Gr\"obner bases in rings with infinitely many variables. Furthermore, we connect the finite and infinite settings by showing that infinite-variable reduced Gr\"obner bases can be characterized via reduced Gr\"obner bases on finite-variable subrings through monomial-order embeddings and filter-based limit constructions.