On the Erdős-Straus Conjecture on Egyptian Fractions

This preprint provides an exhaustive mathematical treatise on the Erdős-Straus Conjecture (Problem #108 in Paul Erdős' collection), formulated by Paul Erdős and Ernst G. Straus in 1948. The conjecture asserts that for every integer n 2, the Egyptian fraction Diophantine equation: 4n = 1x + 1y + 1z admits a solution in positive integers (x, y, z) (N>₀) ³, or equivalently in polynomial form 4xyz = n (xy + yz + xz). Key Mathematical Results Vaughan, 1970). 100% Machine-Checked Verification in Lean 4 Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub: https: //github. com/flouzzy/erdos-problems Primary MSC (2020): 11D68, 11A07, 68V20, 11Y50, 11N36. Keywords: Erdős-Straus Conjecture, Egyptian Fractions, Diophantine Equations, Modular Reduction, Sieve Methods, Formal Verification, Lean 4, Mathlib.