#304: every a/b is a sum of O(log log b) distinct unit fractions — OpenAI's proof of Erdős's 1950 conjecture, with log log F(k) ≍ k (#148) and log log v(k) ≍ k (#293), read by AI seats here, its Lean replayed and bridged to Formal Conjectures

The problems. Erdős problem #304 [ErGr80, p. 37]: "For integers 1 ≤ a < b let N(a,b) denote the minimal k such that there exist integers 1 < n₁ < ⋯ < n_k with a/b = 1/n₁ + ⋯ + 1/n_k. Estimate N(b) = max_1≤a<b N(a,b). Is it true that N(b) ≪ log log b?" Erdős [Er50c] proved log log b ≪ N(b) ≪ log b/log log b, the lower bound already for a = b − 1, and Vose [Vo85] improved the upper bound to N(b) ≪ √(log b). Two neighbours share the paper. #148 [ErGr80, p. 32] asks for good estimates of F(k), the number of solutions of 1 = 1/n₁ + ⋯ + 1/n_k with 1 ≤ n₁ < ⋯ < n_k; the page gives Konyagin's lower bound log log F(k) ≫ k/log k [Ko14] and the Elsholtz–Planitzer upper bound F(k) ≤ c₀^(1/5+o(1))2k [ElPl21], with c₀ written as the Vardi constant 1.264… (Elsholtz and Planitzer's own constant is its square). #293 [ErGr80, p. 35] asks for the growth of v(k), the least integer that does not occur as a denominator in such a k-term solution. Taken literally that is 1 for every k ≥ 2. Erdős and Graham's own wording is "the least integer v(n) > 1" (p. 35), and a December 2025 comment on the thread says that is what is meant, but the page's statement still omits "> 1" and is flagged as ambiguous. Van Doorn and Tang [vDTa25b] proved log v(k) ≫ k² and noted the link to #304 through N(b−1, b). When we fetched them on 21 October, all three pages pointed to the same 14 October exposition of OpenAI's proof by Bloom and van Doorn (UnitFractions.pdf). None had a proof claim, and new comments were suspended. Our earlier work on all three is from 26 July: /report/304 (an exhaustive search proving N(b) ≤ 7 for b ≤ 1000, with equality exactly at b = 733, 739, 787, 839, 863, 898 and 907), /report/148 (F(1), …, F(7) recomputed) and /report/293 (v(1), …, v(7) and 2307 ≤ v(8) ≤ 27539; the forum has since found v(8) = 27,539 and v(9) = 13,856,993).

The claim. OpenAI's family 25, released on 6 October, is one preprint, "Short Egyptian fractions" (25 September, 33 pp). Theorem 1.1: there are absolute constants c₁, c₂ > 0 and b₀ such that c₁ log log b ≤ N(b) ≤ c₂ log log b for every b ≥ b₀. Corollary 1.2: ck ≤ log log F(k) ≤ Ck for every large k. Corollary 1.3: exp(exp(k/600)) ≤ v(k) ≤ 1 + k^2k−1 for every large k, and more precisely log 2/257 ≤ lim inf log log v(k)/k ≤ lim sup log log v(k)/k ≤ log 2. The paper does not compute c₂. The lower bound in Theorem 1.1 is Erdős's, and the upper bounds in the corollaries are elementary. The new content is the uniform upper bound for N(b), which improves (log log b)² (van Doorn and GPT-6 Astra Pro, 16 September; see below), the lower bound log log F(k) ≫ k, which improves Konyagin's k/log k, and the lower bound for v(k), which improves van Doorn and Tang's exp(ck²) and the 16 September exp(exp(√(k/(2c₀)))).

The argument. Put S = log b. Section 2 reduces the upper bound to one proposition. A greedy prefix of O(log S) terms leaves a remainder A/C with A < b and e^D_CS ≤ C < e^2D_CS (Lemma 2.3). Proposition 2.1 then supplies an integer M with e^S < M ≤ e^D_MS and a set G of numerators u ≤ X = e^D_XS, missing at most X/8 of them, such that every u/(MC) with u in G is a sum of at most L log S unit fractions. Take g = ⌊X/(AM)⌋. Of the splits gAM = u + (gAM − u), at most X/4 touch a missing numerator, so one split has both parts in G. Adding the two expansions gives gA/C, and multiplying every denominator by g gives A/C. Takenouchi's 1921 replacements 2/(2p) = 1/(p+1) + 1/(p(p+1)) and 2/(2p+1) = 1/(p+1) + 1/((p+1)(2p+1)) then make the whole list distinct without lengthening it (Lemma 2.2). Sections 3–5 prove the proposition. M is the product of a power of 2 at least S¹⁰⁰⁰⁰⁰ and of primes in [S¹⁰⁰, 2S¹⁰⁰]: m = ⌊S/log S⌋ fixed ones, whose 2^m subset products form a deterministic list of divisors, and 1000 blocks of independently sampled ones, which form random lists. A divisor t of M gives the identity u/(MQ) = 1/((M/t)z) + (1/z)·h/(MQ), with z = ⌈Qt/u⌉ and h = uz − Qt the least residue of −Qt modulo u. One unit fraction thus replaces the numerator u by h. The descent runs through levels X_j = X·e^{−10⁻⁴mj}, j = 0, …, d, with d ≈ D_X·10⁴·log S ≈ 2·10⁹·log S (the paper bounds d by 3D_X·10⁴·log S). At each level, Fourier discrepancy estimates (Section 4) show that for all but an e^−0.001m fraction of u, at least a ρ/2 share of the listed divisors give h below the next level. The danger is that h lands in the failure set of the next level down. Every predecessor of a given pair (h, t) divides Qt + h, so Section 3's uniform bound Σ_h≤Y d_X(N+h)^r ≤ Y·exp(S^1/4) on the r-th moment of the truncated divisor function, for every shift N ≤ e^DS, controls them all at once. With Hölder's inequality it gives the recurrence δ_j ≤ e^−0.001m + e^2S1/4δ_j+1^1−1/r for the failure density, which stays below 1/8 when unrolled over the d levels. Below e^m the random lists reduce every numerator, and the binary expansion over the power of 2 in M finishes. For #148 (Section 6), apply the theorem to (Q−1)/Q with Q the product of the first r odd primes, append 1/Q, remove repetitions while keeping a multiple n of Q (Lemma 6.1), and split n as 1/n = 1/(n+d) + 1/(n+n²/d) over its divisors d. This gives at least 2^r−1 distinct expansions of length O(log r); the padding 1/v = 1/(v+1) + 1/(v(v+1)) on the largest denominator is injective and brings every one to length k. For #293 (Sections 7–8), reserve 1/m and use a greedy prefix that skips m. Its remainder is smaller than every reserved reciprocal, so no expansion of it can reuse a reserved denominator. The explicit slope log 2/257 comes from a second construction built on a quantitative three-primes theorem.

The Lean, and our replay. OpenAI's Lean for this family is two developments that share no imports. OAI/NumberTheory/ShortEgyptian (58 modules, 8,140 lines) proves Theorem 1.1 as OAI.ShortEgyptian.main. OAI/NumberTheory/EgyptianFractions proves nine statements in the namespace OAI.Problem337 (OpenAI's internal label, unrelated to Erdős #337), Theorem 1.1 among them again; the closure of its Main is 290 modules and 36,061 lines (the directory holds 76 more files that Main does not import). We compiled all 348 modules on our machine on 21 October, lake-free and module by module, against Mathlib d13f23b7 from its cache (Lean 4.34.1, openai/math at 1581d4c). There were 0 errors; the build took 15 min 55 s with four workers, with a peak of 6.7 GiB per process. #print axioms on the replayed environment reports exactly the standard axioms propext, Classical.choice and Quot.sound for all ten theorems. Printed under pp.all, the ten theorem statements and the fourteen definitions they use are identical to those of the two comparator challenges, ComparatorChallenges/ShortEgyptianFractions and EgyptianFractions: 24 of 24 blocks match, and the comparators' own copies carry sorryAx, as they should. Two controls behaved: a planted sorry surfaces as sorryAx, and feeding exact_marker_padding the length r = 2, below its hypothesis r ≥ 3, fails to elaborate. The matcher itself was mutation-tested six ways. Mathlib's compiled files came from its cache, so we then started leanchecker --fresh over the closure of Bridge304 and Bridge148_293 below (Mathlib, all 348 of OpenAI's modules and those bridges), which re-checks every declaration from scratch; the later Bridge148LB, which adds Konyagin's form, was compiled after it started. It exited with code 0 after 3,543 s (peak memory 8.2 GiB); a missing-module control exits 1.

Two formalizations, and what they prove on the way. Both developments prove Theorem 1.1 by the paper's §§2–5 route, with the paper's own constants: the dense family, the descent and the divisor moment. Neither takes the shorter §§7–8 route that Bloom and van Doorn extract. In ShortEgyptian the witness for c₁ is 1/2 (the paper's argument gives 1/(1 + log 2)). The witness for c₂ is an explicit real number, upperConstant = greedyConstant + 2·densityConstant ≈ 1.225·10¹⁰ (UpperAssembly.lean, line 52), which the paper never writes down. The threshold b₀ is only shown to exist. Where the paper quotes an outside result, seat L found the Lean proving its own version: a finite cyclic discrepancy lemma for the Erdős–Turán inequality, and Chebyshev bounds for the prime number theorem. It also proves Lemma 6.1 in an exact-length form and Lemma 3.1 for every real r ≥ 0. The one place where the Lean takes a different mathematical route is §8.1. We walked the kernel terms of the nine EgyptianFractions theorems and recorded which modules their constants come from. 233 of the 290 modules contribute. None of the other 57 is used by any of the nine, and they include every three-primes, Vaughan and arc module: Vaughan's identity and a minor-arc bound are proved there, but the major-arc main term appears only as a hypothesis (one docstring reads "no Vinogradov theorem is asserted"). The one used module with "PrimeTriple" in its name, PrimeTripleAsymptotics, only compares growth rates. Proposition 8.1, which gives the slope log 2/257, is instead proved by a "composite cube-free" supply construction that avoids the three-primes theorem altogether (CompositeSupplyFinal.lean; its docstring reads "without any prime-triple distribution premise"). That argument is not in the paper. So the formal certificate covers Corollary 1.3 as stated, but not the paper's own §8.1 argument, which rests on Vinogradov's quantitative three-primes theorem (in the form stated in Kumchev 1997, (1)–(2)) and which seat P read on paper (below). Every ShortEgyptian module is used by main.

Formal Conjectures, and the bridges (ours). Formal Conjectures (FC) records #304 as Erdos304.upper_bound, tagged research solved, with OpenAI's ShortEgyptian/Main.lean linked as its formal proof:

def unitFractionExpressible (a b : ℕ) : Set ℕ :=
  {k | ∃ s : Finset ℕ, s.card = k ∧ (∀ n ∈ s, n > 1) ∧ (a / b : ℚ) = ∑ n ∈ s, (n : ℚ)⁻¹}

noncomputable def smallestCollection (a b : ℕ) : ℕ := sInf (unitFractionExpressible a b)

noncomputable def smallestCollectionTo (b : ℕ) : ℕ :=
  sSup {smallestCollection a b | a ∈ Finset.Ico 1 b}

theorem upper_bound :
    (fun b : ℕ => (smallestCollectionTo b : ℝ)) =O[atTop] (fun b : ℕ => Real.log (Real.log b))

The linked file proves OpenAI's own statement, about strictly increasing lists and a Finset.sup, not this one. Our Bridge304.lean proves, for every a and b, that the two minimal lengths agree. A finite set of denominators is the same thing as its sorted list, and OpenAI's list sum, which Lean elaborates through the coercion List ℕ → List ℚ, equals the finset sum. The bridge also shows that FC's sSup over the image equals OpenAI's Finset.sup. From OAI.ShortEgyptian.main it then derives verbatim copies of upper_bound and of erdos_304.variants.lower_1950, Erdős's lower bound, which FC lists separately (FC already links a third-party formal proof of that one). FC's headline #148 statement is a research-open value question (erdos_148 : (fun k ↦ (F k : ℝ)) =Θ[atTop] erdos_148.answer, with the answer sorried), which log log F(k) ≍ k does not settle. We copy FC's F verbatim and prove that it equals OpenAI's count of strictly increasing tuples, via Finset.orderEmbOfFin. With that we prove two things. One is a verbatim copy of FC's erdos_148.variants.lower_bound, Konyagin's bound exp(exp((log 2·log 3/3 + o(1))·k/log k)) ≤ F(k), tagged research solved but still sorry in FC; it follows from Corollary 1.2 with o = 0. The other is a statement of our own: erdos_148.variants.double_log_order : (fun k ↦ log (log (F k : ℝ))) =Θ[atTop] (fun k ↦ (k : ℝ)). FC has no file for #293. Ours, written in FC's style, defines v k := sInf {m | 2 ≤ m ∧ ∀ S : Finset ℕ, S.card = k → 0 ∉ S → ∑ n ∈ S, 1/n = 1 → m ∉ S} and proves that it equals OpenAI's v. It then proves the explicit bounds exp(exp(k/600)) ≤ v(k) ≤ 1 + k^2k−1 for every large k, and log log v(k) ≍ k; for the upper half we add our own estimate 1 + k^2k−1 ≤ 2^4k. The nine headline bridge theorems, and so every lemma they use, depend on exactly the standard axioms. Five mutated copies make the unchanged proofs fail: FC's definition with n > 0 (which breaks the for-all-a, b bridge lemma at a = b); upper_bound with log log log b; F with 1 ∉ S in place of 0 ∉ S; Konyagin's bound with k·log k in place of k/log k; and log log v(k) ≍ k². They show the proofs are sensitive to those tokens, not that each mutated statement is false. Our script checks the seven copied FC items, and FC's open lines, against FC's text as fetched on 21 October (commit 2a315101), whitespace-normalised, and it fails on a one-token mutation of any copy. These are fresh declarations compiled against OpenAI's Mathlib pin (Lean 4.34.1, Mathlib d13f23b7), not FC's own declarations in FC's repository.

The reading. Four seats, all Claude Opus 5.5, were briefed to refute, to quote the sentence they objected to and to grade each objection: three hostile referees with tools (U, P, W) and one Lean seat (L). A fifth, blind seat checked this page against the files before it went up. The main seat read §2, §5 and §6 itself and found nothing to add. Seat U (§§2–5, the upper bound): HOLDS AS READ. It re-derived the step most likely to break, Lemma 3.1: an r-th moment of the truncated divisor function d_X(N+h) over short shifted intervals, far below the N^ε range of Shiu-type bounds. It works because divisors are cut at X ≤ Y² and the target is only exp(S^1/4). The seat also re-derived (3.3)–(3.13), the Erdős–Turán and van der Corput inputs, the deterministic mean square (D_C = 4D_X is exactly what it needs), the random-product conditioning and the recurrence (5.6)–(5.10). It ran the reduction identity on 200,000 random inputs in exact rational arithmetic; two other checks, of (3.3) and of Lemma 2.3's step bound, carried negative controls that do fail. Its three objections are exposition. Lemma 3.1's proof orders the prime factors "with multiplicity" without saying nondecreasingly, which the next sentence needs. (3.7) uses C_r, the multiplier of (3.5), as an exponent (the proof gives e·C_r). And the outline says "dividing by g" where §2 correctly multiplies the denominators by g. The constant c₂ comes out absolute, at about 1.2·10¹⁰; b₀ is astronomically large, with S ≳ 10³² needed for the recurrence alone. Seat P (§§6–8): HOLDS AS READ. It recomputed 32/log 2 → 16/log 2 → 257/log 2 ≈ 370.8 < 600. It read the statement of Vinogradov's three-primes asymptotic in Kumchev 1997, (1)–(2), and Glibichuk and Konyagin's bilinear bound, and found both used within their hypotheses. It checked the padding injection exhaustively at lengths 3–6, Lemma 7.1 for every m from 4 to 3000, and Lemma 7.2 on 14,309 (expansion, marker) pairs. Its objections: two misleading but correct sentences in §6; an attribution, since Lemma 7.2 is called "the padding lemma of van Doorn and Tang [22, Lemma 2.1]" but its proof is sharper than theirs and rules out a case they treat separately; and ineffective thresholds in §8, harmless because only "sufficiently large k" is claimed. Its main remark is structural. §8 uses nothing from §§3–5, so Corollary 1.3 and the lower bound of Corollary 1.2 (through v(k) ≤ kF(k) + 2) survive any defect there, and so does Theorem 1.1's upper bound, by the adaptation Bloom and van Doorn write out (restarting §8's greedy at b). Seat L (the Lean against the paper and the problems): HOLDS AS READ. The comparator statements say what the paper and the three problems say: n₁ ≥ 2 for #304, n₁ ≥ 1 for #148, and m ≥ 2 for #293. Every junk-value trap is either closed by a proved conjunct (sInf of an empty set, ncard of an infinite set, the real lim inf and lim sup) or harmless by construction (the if inside Finset.sup, log log at small arguments). No axiom, sorry, native_decide, extern, opaque or unsafe appears. Its one caveat, on §8.1, is the dependency finding above, which our walk over the kernel terms confirmed, one module finer (233 used and 57 unused, against L's 234 and 56 from import closures). Seat W (sources and the world) is summarised below. No seat found a FATAL or GAP objection.

Small cases (ours, computational). Two separately written enumerations of the k-term expansions of 1 agree on F(k), on the size of D_k and on v(k) for every k ≤ 6. Route A searches on the remaining fraction and reads the last two terms off the divisors of q²; route B is plain recursion over fractions. Route A alone gives F(7) = 245,765, |D₇| = 83,231 and v(7) = 733. Seat P's enumeration, which uses the same two-term method, agrees on F(7) and v(7), and so do OEIS A006585 and the values on #293's thread. For k ≤ 7, every expansion satisfies n_i ≤ k²ⁱ⁻¹, and F(k) ≤ k^2k−1 and v(k) ≤ 1 + k^2k−1 hold: the bounds the paper and the Lean prove. The largest denominator is s_k − 1 = 1, 6, 42, 1,806, 3,263,442 and 10,650,056,950,806 for k = 1 and 3–7. That is the classical bound n_k ≤ s_k − 1 (Curtiss 1922, recalled by Quanyu Tang on the #293 thread), which the Sylvester expansion 1/2 + 1/3 + 1/7 + ⋯ + 1/(s_k − 1) attains for every k ≠ 2; our search simply agrees with it. An exact search gives N(b) for b ≤ 60, starting 1, 2, 2, 3, 2, 3, 3, 3, 3, 4 at b = 2, …, 11. A search to b ≤ 110 finds the first b with N(b) = 4, 5 and 6 at 11, 17 and 79 (OEIS A097048, a different sequence from A400352 though they share terms); N(b) = 7 first occurs at 733, from our July search. The numerator b − 1 tracks v(k) more closely: the first b with N(b − 1, b) = k is 11, 17, 103 and 733 for k = 4, 5, 6 and 7, which are exactly v(4), …, v(7). Half of this is elementary. For every k, v(k) ≤ min{m : N(m − 1, m) ≥ k}, because a k-term expansion of 1 that contains 1/m leaves (m − 1)/m as a sum of k − 1 distinct unit fractions; this is van Doorn and Tang's reduction, and an open Formal Conjectures PR (#4870) formalizes it. The other inequality fails at k = 3: v(3) = 4, yet N(3, 4) = 2, because the only two-term expansion, 3/4 = 1/2 + 1/4, uses 4 itself. All of these are counts, not evidence for the asymptotic theorems.

Sources and the world. Seat W read every citation it could reach in its primary source. That covers Erdős 1950 (pp. 195 and 199–203), Erdős–Graham (pp. 32, 35, 37–38) and the current v2 of van Doorn and Tang (24 May 2026). It also covers Elsholtz, Elsholtz–Planitzer, Martin, Takenouchi, Nakayama, Erdős–Turán, Kumchev, Kumchev–Tolev and Glibichuk–Konyagin. Each says what the paper takes from it, with the hypotheses it needs. Vose 1985 and Tenenbaum–Yokota were checked only through their zbMATH reviews, Konyagin 2014 only through two secondary sources (mathnet.ru was unreachable), Gallagher 1971 only through its metadata, and Graham–Kolesnik not at all; the paper reproves what it takes from that book. Konyagin's known errata touch nothing the paper uses. Quanyu Tang found on 5 September 2025 that his equation (4) is false, and Konyagin confirmed it, with a missing "m odd" in his Lemma 1, to van Doorn (the #148 thread, 29 December 2025). The paper is dated 25 September; it became public with the release on 6 October (our PDF is byte-identical to the one in openai/math's first commit). Its history skips one public intermediate result. That result grew out of Liam Price's 24 July proof claim on #18, h(n) ≪ (log log n)² for infinitely many practical n, which is about practical numbers and which the paper never addresses. Van Doorn and GPT-6 Astra Pro amended that argument and on 16 September posted "Practical numbers and Egyptian fractions" (formalised by Aristotle), with N(b) ≤ 2c₀(log log b)² and v(k) ≥ exp(exp(√(k/(2c₀)))), c₀ = 14/log 2. That result is strictly weaker than the paper's theorems, so this is a gap in its exposition, not a priority question. Bloom and van Doorn cite it. We found no earlier public claim of any of the three double-logarithmic results. Bloom and van Doorn's exposition flags no mathematical error. It says that the technical arguments of §§3–5, "occupying 15 pages, out of 33 total", are "entirely redundant", because the method the paper uses in §§7–8 (Lemma 7.1's greedy plus §8) gives Theorem 1.1 more simply, and "Strangely, nowhere in the paper is this oddity mentioned". It notes that the lower bound for F(k) follows at once from the one for v(k), since v(k) ≤ kF(k) + 2. It replaces the paper's grouping in §8.2 with base-B digits and the five-product Fourier argument with the Hart–Iosevich sum-product theorem, and gets the length (61/log 2 + o(1))·log log b. Its authors write that they "have not yet read those sections [3–5] in detail". So, as far as we know, §§3–5 have no human reading: apart from our AI seat U, their check is the Lean, as it is for every step this page checks only by machine. On the problems themselves: #304 is answered exactly. #148 and #293 are answered at double-logarithmic precision, which is the order the paper claims, and Erdős and Graham's sharper guesses stay open: their "c₀^2n(1−ε)" for F, and for v(n) the choice between "2^2√n or 2^2n(1−ε)" (p. 35). The paper's lim inf ≥ log 2/257 rules out the first alternative for v and is consistent with the second. #293's ambiguity is that the site's wording drops Erdős and Graham's "least integer v(n) > 1", which makes the literal reading v(k) = 1 for every k ≥ 2. The paper, OEIS A400352 and van Doorn and Tang all use the original definition. By seat W's one-line arguments the other natural readings get the same order: lengths at most k change nothing, since D₁ = D₂ = ∅ and D_k ⊆ D_k+1; with repetitions allowed, D_k only grows, and the denominator bound still holds. In Formal Conjectures, #304's upper_bound is marked research solved with OpenAI's file linked, #148's headline stays research open, and #293 has no file. Issue #476 is open, and PR #6842 (open since 4 October) adds definitions and certificate checks but no growth theorem. That PR "rejects the proposed tuple containing 681943 by checking its exact deficit, 131225/8053056". Its arithmetic on its own tuple is right, and it says itself that rejecting the tuple "does not prove that 681943 cannot occur in another decomposition". But its tuple has 144 and 1984 where the forum certificate (14 September) has 44 and 984, apparently "1/44 + 1/984" misread, and the certificate as posted sums to exactly 1; seat W found this and we re-checked it. The community database (teorth/erdosproblems at 302a00e) still lists all three as open, with status fields dated 31 August 2025.

What this entry is. A referee report on someone else's proof. The theorems, their proofs and their Lean formalizations are OpenAI's, and Bloom and van Doorn's exposition preceded us by a week. Ours: the replay and its controls, the kernel dependency walk, the bridges and their controls, the readings, and the small-case computations. In our labels, the paper's proof is (b): rigorous modulo the prime number theorem, the Erdős–Turán discrepancy inequality and, for the explicit slope log 2/257 only, Vinogradov's three-primes theorem. Where the paper cites an outside result, the Lean either proves its own version (the Erdős–Turán inequality as a finite cyclic discrepancy lemma, the prime number theorem as Chebyshev bounds) or avoids it (the three-primes theorem, see above), so the formal statements depend on nothing beyond Mathlib. The Lean is a machine check of the theorems as stated; it is OpenAI's own, and it is silent on whether the printed text is right. Every seat and the main session were served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.