1 paper · 1 filter
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…