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.

翻译：我们在 Lean4 定理证明器中全面形式化了 Auslander--Buchsbaum--Serre 准则，该准则将正则局部环刻画为具有有限整体维数的诺特局部环。不同于通过正则序列商计算剩余域的投射维数、并利用 Koszul 复形将余切空间维数限制在整体维数内的经典证明，我们的方法系统性地建立在通过 Ext 函子消失定义深度（depth）的形式化基础上。我们建立了关键的同调结果，包括 Rees 定理、Auslander--Buchsbaum 公式和 Ischebeck 定理，并进一步发展了 Cohen--Macaulay 模与环的理论，包括对 Cohen--Macaulay 环的无混合性定理的完整形式化。为证明 Auslander--Buchsbaum--Serre 准则，我们证明了正则局部环上的极大 Cohen--Macaulay 模是自由模，并针对唯一极大理想建立了特定形式的弱化 Ferrand--Vasconcelos 定理。作为推论，我们推导出正则性可在极大理想处检验，并形式化了 Hilbert 合冲定理。这项工作展示了同调代数如何在交换代数的形式化中被有效运用，为该领域的未来发展提供了广泛的基础设施。