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

Abstract

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 Novakovic 2026 (arXiv:2601.16757) records as believed-finite in his own text. The answer is an if-and-only-if characterization, hence strictly stronger than the finiteness being asked about. Contains the paper (LaTeX source + PDF), the Lean 4 proof sources (mathlib v4.34.0, rev 5ed29652, 0 sorry, #print axioms whitelist verified), and the audit evidence (independent final audit verdict, axiom printout, listing-to-source byte verification, named-identifier check, bibliography verification, compile and static-gate logs, roundtrip fidelity record, full novelty search record). The paper is released under CC BY 4.0 and the code under MIT. This artifact was developed with AI assistance under the author's direction; all statements and proofs were checked by the Lean 4 kernel (0 sorry; axioms limited to {propext, Quot.sound, Classical.choice}), and the author is responsible for the final review. The companion priority claim of record for the same kernel result is listed in related_identifiers.