Formalization of Auslander--Buchsbaum--Serre criterion in Lean4

TL;DR

This paper formalizes the Auslander--Buchsbaum--Serre criterion in Lean4, providing a rigorous proof framework for characterizing regular local rings through homological algebra, and develops extensive infrastructure for formalized commutative algebra.

Contribution

It introduces a systematic formalization of key homological results and theorems in commutative algebra within Lean4, including Cohen--Macaulay modules and the regularity criterion.

Findings

Formal proof of Auslander--Buchsbaum--Serre criterion in Lean4

Development of formalized theories of Cohen--Macaulay modules and rings

Verification of Hilbert's Syzygy Theorem

Abstract

We present a comprehensive formalization in the Lean4 theorem prover of the Auslander--Buchsbaum--Serre criterion, which characterizes regular local rings as those Noetherian local rings with finite global dimension. Rather than following the well-known proof that computes the projective dimension of the residue field via quotient by regular sequences and uses the Koszul complex to bound the cotangent space dimension by the global dimension, our approach is built systematically on the formalization of depth defined via the vanishing of Ext functors. We establish key homological results including Rees' theorem, the Auslander--Buchsbaum formula, and Ischebeck's theorem, and further develop the theories of Cohen--Macaulay modules and rings, including a complete formalization of the unmixedness theorem for Cohen--Macaulay rings. To prove the Auslander--Buchsbaum--Serre criterion, we show that maximal Cohen--Macaulay modules over regular local rings are free and establish a weakened form of the Ferrand--Vasconcelos theorem specific for the unique maximal ideal. As corollaries, we deduce that regularity can be checked at maximal ideals and formalize Hilbert's Syzygy Theorem. This work demonstrates how homological algebra can be effectively employed in the formalization of commutative algebra, providing extensive infrastructure for future developments in the field.