HEXAGONbeta

Prime-Generated Localization Descent for Unique Factorization in Lean

Primarily AI-generated textHuman understanding: some partsmath.AC — Commutative Algebracs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗, Anjolina Grisi de Oliveira

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We give a source-grounded exposition of a Lean 4 formalization of prime-generated Nagata factoriality descent. A commutative noetherian integral domain is a unique factorization domain if a localization is a unique factorization domain and every denominator is exactly a finite product of prime elements belonging to the denominator submonoid. The formal statement works with an arbitrary algebra carrying Mathlib’s IsLocalization structure. We explain the two cases for an irreducible element, the multiset cancellation and splitting arguments, and the corollary for submonoids generated by arbitrary sets of primes. A registered polynomial corollary illustrates reuse of the descent package; its Laurent-polynomial premise is proved using Mathlib’s existing polynomial UFD instance, a dependency made explicit here. The exposition is tied to the registered source and dependency pins, distinguishes historical mechanical verification from manuscript review, and situates the development relative to an earlier Lean preprint and an Isabelle/HOL formalization. No new algebraic theorem or priority claim is asserted.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), Ruy J. G. B. de Queiroz (0000-0003-1482-0977), and Anjolina Grisi de Oliveira. The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, inspection and cross-checking of pinned source, exposition, bibliography, and typesetting. Historical pinned metadata separately describes manual mathematical development and OpenAI Codex assistance for repository preparation, statement/proof separation, and reproducibility checks, without a precise model-version attribution for every proof task. Historical mechanical verification is distinguished from manuscript review; no fresh Lean, Comparator, or NanoDa replay was performed here. The exact prime-product denominator hypothesis and the selected polynomial corollary’s dependence on Mathlib’s existing polynomial UFD instance are explicit. The earlier Lean preprint by Arthur Ramos, Ruy de Queiroz, and Anjolina de Oliveira, and the Isabelle/HOL AFP formalization, are credited. No new algebraic theorem, independent polynomial-UFD proof, or priority claim is made. Automated review is not independent human peer review.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion Historical assistance; precise model versions unspecified
Lean
LeanVersion 4.33.0 (registered artifact)

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction–CADE 28, vol. 12699, pp. 625–635. 2021. \urlhttps://doi.org/10.1007/978-3-030-79876-5_37DOI
  2. Nagata, Masayoshi. A remark on the unique factorization theorem. Journal of the Mathematical Society of Japan, vol. 9, no. 1, pp. 143–145. 1957. \urlhttps://doi.org/10.2969/jmsj/00910143DOI
  3. Palomar Registry. Arthur742Ramos/NagataFactoriality. 2026. PALOMAR-2026-08-28-000002, version 1; registered August 28, 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-08-28-000002&version=1link
  4. Palomar Registry. Mechanical verification report for PALOMAR-2026-08-28-000002 version 1. 2026. Checked August 27, 2026, 23:55:51 UTC; historical verification evidence. \urlhttps://data.palomar-registry.org/evidence/PALOMAR-2026-08-28-000002-v1/8ba8ccd66d9c217c4a795335c444c43f0ac06896ce37016e2262784d45dd4638/mechanical-report.jsonlink
  5. Ramos, Arthur F.; de Queiroz, Ruy J. G. B.; de Oliveira, Anjolina G. A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4. 2026. Submitted April 6, 2026. \urlhttps://arxiv.org/abs/2604.05238v1DOI
  6. Ramos, Arthur Freitas; Hulak, David Barros; de Queiroz, Ruy J. G. B. NagataFactoriality: registered Lean source artifact. 2026. Commit 9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7; Apache-2.0. \urlhttps://github.com/Arthur742Ramos/NagataFactoriality/tree/9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7link
  7. Ramos, Arthur Freitas; Hulak, David Barros; de Queiroz, Ruy Jose Guerra Barretto. Nagata Factoriality. 2026. April 20, 2026. Isabelle/HOL formal proof development. \urlhttps://isa-afp.org/entries/Nagata-Factoriality.htmllink
  8. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI
  9. The Stacks Project Authors. Nagata's criterion for factoriality. 2026. Accessed October 1, 2026. \urlhttps://stacks.math.columbia.edu/tag/0AFUlink

Version history

  1. v1Initial depositCurrentOct 01, 2026