A Machine-Checked Modulo 24 Reduction of the Erdős-Straus Conjecture in Lean 4

Abstract

While the global conjecture remains open for a thin set ofprime residues, significant structural progress has been achieved through modular congruencesieves. In this paper, we establish and mechanically verify in the Lean 4 interactive theoremprover (via Mathlib) the Master Modulo 24 Reduction Theorem: every integer n ≥ 2satisfying n ̸≡ 1 (mod 24) possesses an explicit, exact polynomial solution (x, y, z). Thisunconditional result covers 23 out of 24 residue classes modulo 24, demonstrating that theconjecture holds for at least 95.83% of all residue classes. The Lean 4 formalization is verifiedwith zero axioms, zero linter warnings, and zero sorry placeholders, providing an irrefutableproof certificate.