arxiv: 2604.05238 · v1 · submitted 2026-04-06 · 🧮 math.AC · cs.LO

Recognition: 2 theorem links

· Lean Theorem

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4

Arthur F. Ramos , Ruy J. G. B. de Queiroz , Anjolina G. de Oliveira

Authors on Pith no claims yet

Pith reviewed 2026-05-10 18:30 UTC · model grok-4.3

classification 🧮 math.AC cs.LO

keywords Nagata's theoremfactorialityunique factorization domainNoetherian domainLean 4formalizationlocalizationpolynomial ring

0 comments

The pith

Nagata's theorem is formalized in Lean 4: a Noetherian domain is a UFD if it localizes to one at a prime-generated submonoid.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper delivers a formalization in Lean 4 of Nagata's factoriality theorem from commutative algebra. The theorem asserts that if R is a Noetherian domain and S is a prime-generated submonoid such that the localization of R at S is a unique factorization domain, then R is a unique factorization domain. The formalization is presented in both concrete and abstract forms and is used to prove that polynomial rings over Noetherian UFDs are UFDs. It also yields the iterated result for R[X][Y]. The work highlights the necessity of the prime-generated condition on S.

Core claim

The central discovery is a Lean 4 proof of Nagata's theorem: for a Noetherian domain R and a submonoid S generated by primes of R, if S^{-1}R is a UFD then R is a UFD. The development includes applications that recover the UFD property for R[X] when R is a Noetherian UFD, using two different localizations, and extends this to two variables.

What carries the argument

The prime-generated submonoid S, defined so that every element is a finite product of primes in S, which allows the localization to transfer the UFD property back to R.

If this is right

When R is a Noetherian UFD, the ring R[X] is a UFD, shown by localizing at the submonoid of powers of X.
A second proof localizes at the submonoid generated by constant primes and uses the identification with Frac(R)[X].
By applying the theorem twice, R[X][Y] is a UFD whenever R is a Noetherian UFD.
The formalization is reusable through both the concrete Localization construction and the abstract IsLocalization class.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This provides a verified building block for formal proofs involving unique factorization in algebraic geometry or number theory contexts.
The clarification of the submonoid condition may guide refinements in other proof formalizations of similar theorems.
Extensions could include formalizing Nagata's theorem for other classes of rings or properties beyond UFD.

Load-bearing premise

The submonoid S being prime-generated, rather than merely consisting of primes and units, is the load-bearing condition that prevents the statement from being degenerate.

What would settle it

The discovery of a Noetherian domain R and submonoid S not prime-generated where S^{-1}R is a UFD but R is not would demonstrate that the prime-generated hypothesis cannot be dropped.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is a machine-checked Lean 4 formalization of Nagata's theorem that refines the submonoid hypothesis after the weaker version proved degenerate in the formal setting.

read the letter

This paper's main contribution is a machine-checked proof in Lean 4 of Nagata's factoriality theorem, along with a refinement to the prime-generated submonoid condition that the formalization process uncovered as essential. They formalize the result for both concrete localizations and abstract ones, then apply it to show that polynomial rings over noetherian UFDs are UFDs. One proof goes through Laurent polynomials by inverting powers of the variable, and the other identifies the localization with polynomials over the fraction field. The iterated case for two variables follows directly. Since everything is verified in Lean using Mathlib, the proofs are reliable. The work does well by exposing that a prime-or-unit condition on the submonoid is too weak and leads to degeneracy, which is a nice outcome of doing the formalization. It builds directly on existing Mathlib definitions without introducing many new concepts. A soft spot is that the paper itself is short on explanatory text or proof sketches outside the code, so someone not familiar with Lean might not get much from reading it alone. The value is mostly in the accompanying formal library. This is for people in formal mathematics or commutative algebraists who want verified tools for UFD proofs. It would be useful for anyone extending Mathlib with algebra results. The paper deserves a serious referee because the formalization is non-trivial and the refinement improves the theorem statement. I recommend sending it to peer review.

Referee Report

0 major / 3 minor

Summary. The manuscript presents a Lean 4 formalization, built on Mathlib, of Nagata's factoriality theorem: if R is a Noetherian domain and S is a prime-generated multiplicative submonoid such that S^{-1}R is a UFD, then R is a UFD. The development supplies both a concrete formulation via Localization and an abstract one via IsLocalization; it includes two applications establishing that R[X] is a UFD whenever R is a Noetherian UFD (one via localization at powers of X, one via constant primes and identification with Frac(R)[X]), plus the iterated corollary for R[X][Y]. The prime-generated hypothesis is highlighted as a refinement that the formalization effort revealed to be necessary, since a prime-or-unit variant is degenerate.

Significance. If the formalization is correct, the work supplies machine-checked proofs of a standard but non-trivial result in commutative algebra, together with reusable infrastructure for localizations and UFDs. The applications to polynomial rings demonstrate modularity and immediate utility. The explicit refinement of the prime-generated condition, discovered during formalization, adds mathematical value beyond mere verification. Such developments provide independent, checkable support for theorems that are frequently invoked in algebraic geometry and number theory.

minor comments (3)

The claim that no public formalization exists in Lean, Coq, or Isabelle would be strengthened by a brief description of the search performed (e.g., keywords, repositories checked, and date).
[applications section] In the applications section, the two distinct proofs that R[X] is a UFD would benefit from an explicit side-by-side comparison of the hypotheses used in each route and the precise statements of the resulting corollaries.
A short table or list of the key Mathlib declarations and instances imported (e.g., for IsLocalization, UFD, Noetherian) would improve readability and reproducibility for readers who wish to inspect or extend the code.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, the assessment of significance, and the recommendation of minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity: machine-checked formalization of known theorem

full rationale

The paper is a Lean 4 Mathlib formalization of Nagata's classical factoriality theorem (Noetherian domain R with prime-generated submonoid S such that S^{-1}R is UFD implies R is UFD). All derivations consist of machine-verified proofs built from standard Mathlib definitions of rings, domains, UFDs, localizations, and IsLocalization. The prime-generated hypothesis was refined during formalization to avoid degeneracy, but this is an empirical improvement exposed by the checker rather than a definitional loop. No predictions, fitted parameters, or load-bearing self-citations reduce the target statement to its inputs by construction; the Lean kernel supplies independent verification against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The formalization rests on standard Mathlib definitions of noetherian domains, UFDs, submonoids, and localizations; no new free parameters, ad-hoc axioms, or invented entities are introduced beyond the classical statement.

axioms (1)

standard math Standard definitions of noetherian domain, UFD, prime element, and localization in commutative algebra
Invoked throughout the development as background from Mathlib

pith-pipeline@v0.9.0 · 5500 in / 1196 out tokens · 52179 ms · 2026-05-10T18:30:55.814336+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem 3.3 (Nagata): Let R be a noetherian integral domain and S ⊆ R a prime-generated submonoid. If the localization S⁻¹R is a UFD, then R is a UFD.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

PrimeGenerated predicate using Multiset factorization of denominators

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

15 extracted references · 8 canonical work pages

[1]

Baanen, S.R

A. Baanen, S.R. Dahmen, A. Narayanan, and F.A.E. Nuccio Mortarino Majno di Capriglio. A formalization of Dedekind domains and class groups of global fields.J. Automated Reasoning, 66:611–637, 2022.https://doi.org/10.1007/s10817-022-09644-0

work page doi:10.1007/s10817-022-09644-0 2022
[2]

A. Bordg. The localization of a commutative ring.Archive of Formal Proofs, June 2018. https://www.isa-afp.org/entries/Localization_Ring.html

2018
[3]

A. Best, C. Birkbeck, R. Brasca, E. Rodriguez Boidi, R. Van de Velde, and A. Yang. A complete formalization of Fermat’s Last Theorem for regular primes in Lean.Annals of Formalized Mathematics, 1:103–132, 2025.https://doi.org/10.46298/afm.14586

work page doi:10.46298/afm.14586 2025
[4]

Divasón, S.J.C

J. Divasón, S.J.C. Joosten, R. Thiemann, and A. Yamada. A verified implementation of the Berlekamp–Zassenhaus factorization algorithm.J. Automated Reasoning, 64:699–735, 2020. https://doi.org/10.1007/s10817-019-09526-y

work page doi:10.1007/s10817-019-09526-y 2020
[5]

Kaplansky.Commutative Rings

I. Kaplansky.Commutative Rings. Allyn and Bacon, 1970

1970
[6]

Loeffler and M

D. Loeffler and M. Stoll. Formalizing zeta andL-functions in Lean.Annals of Formalized Mathematics, 1:43–56, 2025.https://doi.org/10.46298/afm.15328

work page doi:10.46298/afm.15328 2025
[7]

The Lean mathematical library

The mathlib Community. The Lean mathematical library. InProc. 9th ACM SIGPLAN Int. Conf. Certified Programs and Proofs (CPP 2020), pages 367–381, 2020.https://doi.org/10. 1145/3372885.3373824

work page arXiv 2020
[8]

Mahboubi and E

A. Mahboubi and E. Tassi.Mathematical Components. Zenodo, 2022.https://doi.org/10. 5281/zenodo.3999478

2022
[9]

Matsumura.Commutative Ring Theory

H. Matsumura.Commutative Ring Theory. Cambridge Studies in Advanced Mathematics, vol. 8. Cambridge University Press, 1989

1989
[10]

L.de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In A. Platzer and G. Sutcliffe, editors,Proc. 28th Int. Conf. Automated Deduction (CADE-28), LNAI 12699, pages 625–635. Springer, 2021.https://doi.org/10.1007/978-3-030-79876-5_37

work page doi:10.1007/978-3-030-79876-5_37 2021
[11]

M. Nagata. A remark on the unique factorization theorem.J. Math. Soc. Japan, 9:143–145, 1957.https://doi.org/10.2969/jmsj/00910143

work page doi:10.2969/jmsj/00910143 1957
[12]

Nagata.Local Rings

M. Nagata.Local Rings. Interscience Tracts in Pure and Applied Mathematics, No. 13. Interscience Publishers, New York, 1962

1962
[13]

J. Riou. Formalization of derived categories in Lean/mathlib.Annals of Formalized Mathematics, 1:1–42, 2025.https://doi.org/10.46298/afm.13609

work page doi:10.46298/afm.13609 2025
[14]

Samuel.Lectures on Unique Factorization Domains

P. Samuel.Lectures on Unique Factorization Domains. Lectures on Mathematics and Physics, No. 30. Tata Institute of Fundamental Research, Bombay, 1964. 22

1964
[15]

edu, 2024

The Stacks Project Authors.The Stacks Project, Tag 0AFU.https://stacks.math.columbia. edu, 2024. Accessed: 2026-04-05. 23

2024