Short Egyptian fractions

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

$First page of Short Egyptian fractions$

Short Egyptian fractions

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Short-Egyptian-fractions-September-25-2026,
  author = {{OpenAI}},
  title = {{Short Egyptian fractions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf}{OAI:Short-Egyptian-fractions-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Short Egyptian fractions

Scope

An Egyptian-fraction expansion writes a rational number as a sum of distinct unit fractions. The formalization proves that every $a/b$ with $1\le a<b$ has such an expansion and that the largest minimum length at denominator $b$ is $\Theta(\log\log b)$. If $F(k)$ counts exact $k$-term expansions of $1$, it also proves $\log\log F(k)=\Theta(k)$ and bounds every denominator in such an expansion.

Every integer $m\ge2$ occurs as a denominator in an expansion of $1$, with length eventually at most $(257/\log2+\varepsilon)\log\log m$ for every $\varepsilon>0$; padding can preserve that denominator. If $v(k)$ is the least integer at least $2$ absent from all exact $k$-term expansions of $1$, then eventually $e^{e^{k/600}}\le v(k)\le1+k^{2^{k-1}}$, and $\liminf_{k\to\infty}\log\log v(k)/k\ge\log2/257$.

Comparator links

Result	Comparator statement
Short expansions, counting, and prescribed denominators	EgyptianFractions.lean
Optimal order of the shortest Egyptian-fraction expansions	ShortEgyptianFractions.lean

Scope note on GitHub →