{"id":"arxiv/2604.05238","url":"https://arxiv.org/abs/2604.05238","tags":["math.AC","cs.LO"],"score":0,"title":"A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4","domain":"math.AC","source":"arxiv","authors":["Arthur F. Ramos","Ruy J. G. B. de Queiroz","Anjolina G. de Oliveira"],"reviews":0,"subject":"math.AC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-06","reactions":{}}