Short Egyptian fractions

Every rational a/b with 1\le a\lt b is a sum of O(\log\log b) distinct positive unit fractions. The worst-case minimum number of terms has the same order, resolving Erdős’s conjecture on short Egyptian fractions. (Lean)

Manuscript

Short Egyptian fractions

September 25, 2026 · source · Lean formalization available · cite as \cite{OAI:Short-Egyptian-fractions-September-25-2026}

We prove a conjecture of Erdős: for every sufficiently large integer b, every rational number a/b with 1\le a\lt b is a sum of O(\log\log b) distinct positive unit fractions, with an absolute implied constant. This order is best possible when the numerator varies. We also show that both the number of expansions of 1 with exactly k distinct terms and the least integer at least 2 that never occurs as a denominator in such an expansion grow doubly exponentially in k: their double logarithms have order k.

Result 025 · Number theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.