The Diophantine equation x^2 = n! * n#: the complete solution set, formalized and machine-checked in Lean 4 (paper + artifact, AI4Math pipeline)

形式化数学论文与工件:丢番图方程 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 逐字节核验、参考文献核验、C9 新颖性查新全量记录)。论文以 CC-BY-4.0 许可,代码以 MIT 许可。本工件由 AI4Math 高度自动化流水线产出(LLM 生成 + Lean kernel 编译裁决),全部入库证明 0 sorry、公理限 {propext, Quot.sound, Classical.choice},由作者本人终审负责。姊妹优先权存缴记录(claim of record)见 related_identifiers。