Erdős's conjecture on short Egyptian fractions

An Egyptian-fraction expansion writes a positive rational number as a sum of distinct unit fractions. Erdős conjectured that every a/b with 1 ≤ a < b has such an expansion with O(log log b) terms (Erdős problem 304); Erdős and Graham also asked how many expansions of 1 have exactly k terms (problem 148) and which denominators occur in them (problem 293). A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims all three, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

As recounted in the introduction of the manuscript:
- Erdős reported de Bruijn's bound for the maximal minimum length N(b) and improved it to O(log b/log log b), proposed the double-logarithmic bound and proved the matching lower order; Vose obtained O(√log b). Tenenbaum and Yokota controlled the length and the size of the denominators simultaneously.
- For the number F(k) of k-term expansions of 1, Konyagin and Elsholtz gave lower bounds with double logarithm of order k/log k, and Elsholtz and Planitzer an upper bound with double logarithm O(k). For the least integer v(k) absent from all k-term expansions of 1, van Doorn and Tang proved v(k) ≥ e^ck² and anticipated the link with uniform short expansions.

The original result

Claim. Theorem 1.1 of Short Egyptian fractions states that there are absolute constants c₁, c₂ > 0 such that c₁ log log b ≤ N(b) ≤ c₂ log log b for all large b, where N(b) is the largest, over 1 ≤ a < b, of the least number of terms in an expansion of a/b. Corollaries give log log F(k) of order k and log log v(k) of order k, with explicit constants in the bounds for v(k).
Method, as described: after a bounded number of greedy steps, the remainder is written with a denominator in a prescribed range; an auxiliary integer is constructed so that almost every fraction in a large interval of numerators has a short expansion, obtained by descending through numerator ranges, and the remaining numerator is a sum of two numerators from this dense family.
Sources. The manuscript Short Egyptian fractions at commit 1581d4c.
Formalization, as described by the repository. The scope note states that the formalization proves that the largest minimum length at denominator b is of order log log b, that log log F(k) is of order k, and the stated bounds for prescribed denominators. The Comparator statements are EgyptianFractions.lean and ShortEgyptianFractions.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 21 October 2026)
2026-10-07	eigendash/openai-math-visualised (GitHub; commit `021c0f8`)	Numerical illustration	Computes the exact maximal minimum length N(b) for b ≤ 220, with N(b)/log log b between 2.43 and 4.80.	Repository; it states that agreement with an asymptotic law is evidence about the statement, not about the proof.
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit `c76f1e4`, 14 October 2026)	Review (fidelity of the formal statement)	Rates the family "full" with no note, the expansions being stated with plain lists of strictly increasing natural numbers and rational sums, and records sandboxed Comparator passes for `EgyptianFractions` and `ShortEgyptianFractions`.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08	T. F. Bloom, Erdős problems in the OpenAI proofs (blog post on erdosproblems.com), entry for problems 148, 293 and 304	Catalogue (remark)	Lists the three claims, notes that the proofs have been formalised, that the manuscript mostly establishes the first theorem and deduces the other two, and that it appears to use many of the usual methods of the subject.	Blog post, read on 21 October 2026, which the author says he will update. The author states that he had not yet examined the proofs or checked the Lean files and that the post is not an endorsement.
2026-10-09	W. van Doorn, Short Egyptian fractions (Woett/Mathematical-shorts, commit `a65db1e`)	Exposition (simplified proof)	A human-written exposition and simplification of the proof of the first theorem, giving at most (16/log 2 + o(1)) log log b terms. In comments on the blog post above, the author discusses which arguments of the manuscript its Lean formalizations follow.	Note; the author states on the blog that it was written with the help of ChatGPT.
2026-10-10 (current file dated 15 October 2026)	T. F. Bloom, W. van Doorn, Optimal bounds for the length and number of unit fraction representations (PDF on erdosproblems.com)	Exposition (simplified proofs)	A human-written exposition and simplification of the proofs of all three results, with a section comparing them with the manuscript's proofs; the authors describe the manuscript as difficult to read and as containing much unnecessary material.	15-page PDF hosted on erdosproblems.com.
2026-10-10	cert-machine, openai/math lane K: runs 38019899278 and 38051470892	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the `ShortEgyptianFractions` solution, in 443 s, and the `EgyptianFractions` solution, in 745 s.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions (time-outs, memory, errors) lists neither `EgyptianFractions` nor `ShortEgyptianFractions`, so both were accepted by con-leche and by Lean's official kernel.	Development journal.

Notes

The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.