Aurora0134

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

形式化数学论文与工件:丢番图方程 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,#pri...

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

Formalized-mathematics paper and artifact: the complete solution set of the Diophantine equation x^2 = n!! * lcm(1..n) (double factorial times least common multiple) over the natural numbers -- exactly n in {0,1,2,5,7} (with x = 1,1,2,30,210), the second of the two cases that Nov...