The Diophantine equation x^2 = n! * n#: the complete solution set, formalized and machine-checked in Lean 4

Abstract

形式化数学论文与工件:丢番图方程 x^2 = n! * n#(阶乘乘 primorial)在 n 为自然数时的完全解集——恰为 n in {0,1,2,3,4,5}(x = 1,1,2,6,12,60),系 Novaković 2026(arXiv:2601.16757)正文自陈未解情形之一的完全答案。含论文 LaTeX 源与 PDF、Lean 4 证明源码(mathlib v4.34.0,rev 5ed29652,0 sorry,#print axioms 白名单核验)、审计证据(终裁书、良定义门输出、公理打印实录、listing 逐字节核验、参考文献核验、新颖性查新全量记录)。论文以 CC-BY-4.0 许可,代码以 MIT 许可。本工件在作者主导下借助 AI 辅助开发;全部命题与证明经 Lean 4 kernel 编译核验(0 sorry,公理限 {propext, Quot.sound, Classical.choice}),由作者本人终审负责。姊妹优先权存缴记录(claim of record)见 related_identifiers。