Every natural number is a sum of distinct semiprime unit fractions

Abstract

We prove that every natural number is a finite sum of distinct unit fractions whose denominators are semiprimes (products of two distinct primes). This is the $\omega =2$ integer case of a problem of Erdős and Graham, stated only as a conjecture by Butler, Erdős and Graham (Integers 15 (2015), A51), who proved the $\omega =3$ analogue. Counterintuitively the problem hardens as $\omega$ decreases -- the induction's feed thins -- so $\omega =2$ is the hard case; our proof adapts the Butler-Erdős-Graham induction to this thin-feed regime, where the entire content of the induction step reduces to an explicit onset inequality $Y_0(N)\le \min \{\beta (N),{\beta }^{\prime }(N)\}$, proved for all $N\ge 10$ by Olson's addition theorem and elementary Chebyshev bounds above a finite, machine-checked base range. The same engine extends to the rationals: for every squarefree $b$, every $a/b$ above an explicit threshold $\min \{B_{N_b}/6,1/5\}$ is $\omega =2$ representable, unconditionally. As an application we give the first complete proof of the rational $\omega =3$ statement -- every $a/b$ with squarefree $b$ is a sum of distinct sphenic unit fractions -- that Butler, Erdős and Graham conjectured but left unpublished; a descent settles every $\omega \ge 3$. What remains open is the $\omega =2$ regime below this threshold, which we reduce to a single explicit conjecture -- that the gap-free floor of a semiprime subset-sum set tends to zero. This work is a human-AI collaboration: AI tools (notably Anthropic's Claude, used through Claude Code) contributed substantially to the Lean formalisation, the experiments, and the writing; correspondingly, every result is machine-checked in Lean 4 / Mathlib (no sorry; two cited classical axioms, plus the native_decide compiler-trust base for the finite computations), so its correctness is independent of the tools used.

22 pages. Human-AI collaboration; see the "Use of AI" statement. Companion Lean 4 / Mathlib formalisation (0 sorry; reduces to two cited classical axioms plus the native_decide compiler-trust base) and standard-library Python verification scripts are included as ancillary files