---

Claim. D. Michael Piscitelli's Lean 4 development herakles-dev/erdos672-four-squares-lean, first posted on 10 September 2026, proves erdos_672_variants_euler : Erdos672With 4 2, the case $k=4$, $\ell=2$ of Problem 672: the product $n(n+d)(n+2d)(n+3d)$ of a progression of positive integers with $\gcd(n,d)=1$ is never a perfect square. Its definitions of Erdos672With and Set.IsAPOfLengthWith are copied from the formal-conjectures statement file, and the theorem reduces to ap4_prod_ne_sq, Euler's theorem in concrete form, which in turn rests on no_four_squares_in_ap, Fermat's theorem that no four squares form an arithmetic progression, proved by infinite descent from scratch. The repository's write-up says the proof was developed with Claude Code. The site credits the case to Euler, with no publication named; this page records the formal proof, an independent proof of that case. On 18 September 2026 the formal-conjectures statement of the variant erdos_672.variants.euler gained a formal_proof link to this file.

Covers. Length $k=4$ with exponent $\ell=2$ (and so every even exponent). Not covered: every other length, and $k=4$ with odd exponents.

Depends on. Nothing in this wiki.

Standing. Claimed. The repository's README reports a sorry-free build whose #print axioms shows only propext, Classical.choice and Quot.sound; this corpus has not built or audited the development, so it gives no formalized evidence. The four-term case is also inside the refereed Győry–Hajdu–Saradha theorem, whose proof takes it from Euler.