collaborators

1 paper

math.AC2025

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

Naillin Guan, Yongle Hu

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…