@article{nagata1957,
 author={Nagata, Masayoshi},
 title={A remark on the unique factorization theorem},
 journal={Journal of the Mathematical Society of Japan},
 volume={9}, number={1}, pages={143--145}, year={1957},
 doi={10.2969/jmsj/00910143},
 url={https://doi.org/10.2969/jmsj/00910143},
 note={\url{https://doi.org/10.2969/jmsj/00910143}}
}
@misc{stacks,
 author={{The Stacks Project Authors}},
 title={Nagata's criterion for factoriality},
 howpublished={The Stacks Project, Lemma 10.120.7, Tag 0AFU},
 year={2026}, note={Accessed October 1, 2026. \url{https://stacks.math.columbia.edu/tag/0AFU}},
 url={https://stacks.math.columbia.edu/tag/0AFU}
}
@misc{leanpreprint,
 author={Ramos, Arthur F. and de Queiroz, Ruy J. G. B. and de Oliveira, Anjolina G.},
 title={A Prime-Generated Formalization of {Nagata}'s Factoriality Theorem in {Lean} 4},
 year={2026}, howpublished={arXiv:2604.05238v1},
 note={Submitted April 6, 2026. \url{https://arxiv.org/abs/2604.05238v1}},
 doi={10.48550/arXiv.2604.05238},
 url={https://arxiv.org/abs/2604.05238v1}
}
@misc{afp,
 author={Ramos, Arthur Freitas and Hulak, David Barros and de Queiroz, Ruy Jose Guerra Barretto},
 title={{Nagata} Factoriality},
 howpublished={Archive of Formal Proofs}, year={2026},
 note={April 20, 2026. Isabelle/HOL formal proof development. \url{https://isa-afp.org/entries/Nagata-Factoriality.html}},
 url={https://isa-afp.org/entries/Nagata-Factoriality.html}
}
@inproceedings{mathlib,
 author={{The mathlib Community}},
 title={The {Lean} Mathematical Library},
 booktitle={Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 pages={367--381}, year={2020},
 doi={10.1145/3372885.3373824},
 url={https://doi.org/10.1145/3372885.3373824},
 note={\url{https://doi.org/10.1145/3372885.3373824}}
}
@inproceedings{lean4,
 author={de Moura, Leonardo and Ullrich, Sebastian},
 title={The {Lean} 4 Theorem Prover and Programming Language},
 booktitle={Automated Deduction---CADE 28},
 series={Lecture Notes in Computer Science}, volume={12699},
 pages={625--635}, publisher={Springer}, year={2021},
 doi={10.1007/978-3-030-79876-5_37},
 url={https://doi.org/10.1007/978-3-030-79876-5_37},
 note={\url{https://doi.org/10.1007/978-3-030-79876-5_37}}
}
@misc{artifact,
 author={Ramos, Arthur Freitas and Hulak, David Barros and de Queiroz, Ruy J. G. B.},
 title={{NagataFactoriality}: registered {Lean} source artifact},
 year={2026}, note={Commit 9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7; Apache-2.0. \url{https://github.com/Arthur742Ramos/NagataFactoriality/tree/9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7}},
 url={https://github.com/Arthur742Ramos/NagataFactoriality/tree/9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7}
}
@misc{palomar,
 author={{Palomar Registry}},
 title={{Arthur742Ramos/NagataFactoriality}},
 year={2026}, note={PALOMAR-2026-08-28-000002, version 1; registered August 28, 2026. \url{https://palomar-registry.org/entry?id=PALOMAR-2026-08-28-000002&version=1}},
 url={https://palomar-registry.org/entry?id=PALOMAR-2026-08-28-000002&version=1}
}
@misc{mechanical,
 author={{Palomar Registry}},
 title={Mechanical verification report for {PALOMAR-2026-08-28-000002} version 1},
 year={2026}, note={Checked August 27, 2026, 23:55:51 UTC; historical verification evidence. \url{https://data.palomar-registry.org/evidence/PALOMAR-2026-08-28-000002-v1/8ba8ccd66d9c217c4a795335c444c43f0ac06896ce37016e2262784d45dd4638/mechanical-report.json}},
 url={https://data.palomar-registry.org/evidence/PALOMAR-2026-08-28-000002-v1/8ba8ccd66d9c217c4a795335c444c43f0ac06896ce37016e2262784d45dd4638/mechanical-report.json}
}