Paper 117 (draft): Erdős-Straus Conjecture — Lean 4 Small-n Formalization + Infinite Mod-4 Family
The Erdős-Straus conjecture (1948) states that for every integer n ≥ 2 there exist positive integers a, b, c with 4/n = 1/a + 1/b + 1/c. It is empirically verified for n < 10^17 (Salez and others) and closed for many residue classes, but remains open in full generality. We pro...