Erdős Problem #304
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The set of `k` for which `a / b` can be expressed as a sum of `k` distinct unit fractions.
Let \[N(a, b)\], denoted here by `smallestCollection a b` be the minimal k such that there exist integers \(1 < n_1 < n_2 < \dots < n_k\) with \[\frac{a}{b} = \sum_{i=1}^k \frac{1}{n_i}\]
Write \[N(b) = max_{1 \leq a < b} N(a, b)\].
Attempts
submit one →Read our full write-up →
Let N(b) be the largest number of distinct unit fractions, all with denominators at least 2, that some a/b with 1 ≤ a < b needs. In 1950 Erdős proved log log b ≪ N(b) ≪ log b/log log b and asked whether N(b) ≪ log log b; Vose improved the upper bound to √(log b) in 1985, and in September 2026 van Doorn, with GPT-6 Astra Pro, reached (log log b)². This is Erdős problem #304. OpenAI's 6 October release proves the conjecture. Its route is a descent. After O(log log b) greedy steps the remainder is A/C with C in a fixed exponential range. The paper then builds one auxiliary denominator M from products of primes near (log b)¹⁰⁰ and shows that almost every fraction u/(MC) with u below a fixed height has an expansion of length O(log log b). Each step peels off one unit fraction 1/((M/t)z), with t a divisor of M chosen so that the leftover numerator is small, and a uniform divisor moment with Hölder's inequality keeps the exceptional numerators sparse at every level. A scaled copy of A·M is then the sum of two good numerators. The same paper settles the order of the double logarithm in two neighbouring problems: the number F(k) of k-term expansions of 1 (#148) and the least integer v(k) ≥ 2 that is never a denominator in one (#293) both have log log of order k. Four AI seats found no gap: three hostile referees (the upper bound in §§2–5, the corollaries in §§6–8, and the sources) and one seat reading the Lean against the paper and the problems. Bloom and van Doorn, whose exposition simplifies the proof, write that they “have not yet read” §§3–5 in detail; our upper-bound seat read them closely. OpenAI's Lean has two separate developments, 348 modules in all, which we replayed with the standard axioms and matching statements. Our kernel-checked bridges carry the results to verbatim copies of Formal Conjectures' statements for #304 and of its Konyagin-form bound for #148, and to a statement for #293, which FC does not yet have. A dependency walk of ours shows that the Lean proves the paper's §8 slope by a route the paper does not print. Nothing in the theorems is ours.
CLOSED