Formalization of Auslander-Buchsbaum-Serre criterion in Lean4. - Naillin Guan; Yongle Hu (CoRR, 2025)