A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Abstract
We present a Lean 4 Mathlib formalization of Nagata's factoriality theorem: if R is a noetherian domain and S <= R is a prime-generated submonoid such that S^{-1}R is a UFD, then R itself is a UFD. The prime-generated hypothesis -- every element of S is a finite product of primes belonging to S -- replaces a superficially cleaner but degenerate prime-or-unit condition that the formalization effort exposed. The development packages the theorem both for the concrete type Localization S and through abstract IsLocalization formulations. As applications, we formalize two Nagata-based proofs that R[X] is a UFD whenever R is a noetherian UFD: one via Laurent-polynomial localization at powers of X, and one via localization at the constant primes and identification with Frac(R)[X]. Reusing the same package, we also obtain the iterated polynomial corollary R[X][Y]. No public formalization of this result is known to us in Lean, Coq, or Isabelle.
Keywords
Cite
@article{arxiv.2604.05238,
title = {A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4},
author = {Arthur F. Ramos and Ruy J. G. B. de Queiroz and Anjolina G. de Oliveira},
journal= {arXiv preprint arXiv:2604.05238},
year = {2026}
}
Comments
23 pages. Formalization artifact available at https://github.com/Arthur742Ramos/NagataFactoriality (tagged afm-submission-draft-2026-04-04). Lean 4.24.0, Mathlib. No sorry/admit/axiom placeholders. 97 theorem/lemma declarations, 1352 lines of Lean source across 18 files