Charles EDOU NZE

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

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 Modul...