AI Proved What?

Episode 025, October 2026

How few fractions?

Short Egyptian fractions

Covers result 025 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

4:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Unit fractions
  2. 0:47How short?
  3. 1:44The claim
  4. 2:44How the proof goes
  5. 3:52Where it stands

The claim, in plain words

An Egyptian fraction writes a number as a sum of distinct unit fractions, like 2/5 = 1/3 + 1/15. Every fraction between 0 and 1 can be written this way, but how many terms are needed? Let N(b) be the largest number of terms that any fraction a/b with 1 ≤ a < b needs.

Result 025 (33 pages) claims that, for all large b, every a/b is a sum of at most a constant times log log b distinct unit fractions. Together with Erdős’s lower bound, this gives c1 log log b ≤ N(b) ≤ c2 log log b, answering Erdős’s conjecture (Erdős problem #304). Two consequences follow.

  • The number F(k) of ways to write 1 as a sum of k distinct unit fractions satisfies log log F(k) ≍ k.
  • The smallest integer v(k) ≥ 2 that never appears as a denominator in such a sum also grows doubly exponentially: eek/600 ≤ v(k) ≤ 1 + k2k−1 for large k (see problem #293).

What it doesn’t claim

The constant in front of log log b is not computed, and neither is the point from which the bound holds. The denominators are unrestricted and may be huge. Tenenbaum and Yokota, by contrast, bound the length by about log b/log log b while also keeping every denominator below about 4b(log b)2 log log b; the new result does not control denominator size.

Where it stands

Posted as a preprint
OpenAI, dated September 25, 2026, released October 6; 33 pages
Peer reviewed
Not yet
Checked in Lean
By OpenAI (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and we found no public response; erdosproblems.com still lists problem #304 as open. OpenAI’s Lean statements (the order of N(b) and the counting and denominator corollaries) match the paper’s Theorem 1.1 and Corollaries 1.2 and 1.3. The two formalizations together come to about 350 files and 44,000 lines, not counting Mathlib, with no unfinished proofs (sorry). The main statements are listed in OpenAI’s formalization catalog, whose review status is “unchecked”.

What was known

  • Fibonacci’s greedy method (1202) always produces an expansion, but the denominators can explode: on 5/121 it gives five terms, the last with 25 digits, while 1/33 + 1/121 + 1/363 works.
  • Sylvester’s sequence 2, 3, 7, 43, 1807, … gives the closest approach to 1 from below by k unit fractions (Curtiss, 1922): 1/2 + 1/3 + 1/7 + 1/43 = 1 − 1/1806. So (b − 1)/b needs about log log b terms or more; for a googol, at least 9.
  • Erdős (1950) proved that lower order and the upper bound N(b) ≪ log b/log log b, and conjectured log log b. Vose (1985) proved N(b) ≪ √(log b).

How the proof goes

  1. Greedy start. With S = log b, about log S greedy steps either finish or leave a fraction A/C with C in a chosen range.
  2. A helper number. The proof builds an integer M with many divisors from products of primes. For a numerator u and a divisor t of M, the identity u/(MQ) = 1/((M/t)z) + h/(zMQ), with z = ⌈Qt/u⌉, peels off one unit fraction and leaves the residue h ≡ −Qt mod u. The primes are chosen, deterministically at large ranges and at random at small ones, so that small residues are common.
  3. The descent. Descending through about log S numerator ranges, some numerators fail. A uniform moment bound for the small divisors of numbers in a shifted interval, with Hölder’s inequality, keeps the failures a small fraction at every level. Almost every numerator in a long interval gets a short expansion.
  4. Every numerator. A multiple gAM is written as the sum of two numerators from that family. Adding their expansions and dividing by g represents A/C.

The numbers in the video

  • A short Python script checks the greedy and three-term expansions of 5/121, Sylvester’s sums 1 − 1/(sk+1 − 1), and the best approach to 1 with two and three terms by exhaustive search.
  • It also checks the nine-term lower bound for a googol, F(k) = 1, 0, 1, 6, 72, 2,320 for k = 1, …, 6 (with 245,765 and 151,182,379 from OEIS A006585), and v(3) = 4, v(4) = 11.
  • The googol comparison (42.3, 15.2 and 5.4) compares the shapes of the bounds, with constants set to 1.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00Unit fractions

Egyptian scribes wrote fractions mostly as sums of distinct unit fractions: 2/5 is 1/3 + 1/15. Every fraction between zero and one can be written this way. The greedy method, described by Fibonacci in 1202, keeps taking the largest unit fraction that fits. But greedy can explode. On 5/121 it takes five terms, and the last denominator has 25 digits. Yet 1/33 + 1/121 + 1/363 already works. So how many terms do you really need? Result 025 in OpenAI’s math repository claims the answer to a question Erdős raised in 1950.

0:47How short?

Fix the denominator b, and let N(b) be the most terms any numerator over b needs. Some fractions force many terms. Take Sylvester’s sequence, 2, 3, 7, 43, each one more than the product of the ones before. Their reciprocals get as close to one, from below, as that many unit fractions can: 1/2 + 1/3 + 1/7 + 1/43 = 1 − 1/1806. The sequence roughly squares at each step. So writing (b − 1)/b takes about log log b terms or more. For b a googol, at least 9. In 1950, Erdős proved that lower bound, showed that N(b) is at most about log b / log log b, and conjectured that log log b is the truth. In 1985, Michael Vose brought the bound down to about the square root of log b. The question is Erdős problem 304, still listed as open.

1:44The claim

The preprint, 33 pages, dated September 25, claims Erdős’s conjecture: every fraction a/b, with b large and a less than b, is a sum of at most a constant times log log b distinct unit fractions. With the lower bound, N(b) grows like log log b, up to constant factors. For a googol, comparing shapes only, with constants set to one: log b / log log b is about 42, the square root of log b about 15, and log log b about 5.4. Two consequences follow. The number of ways to write one as a sum of k distinct unit fractions grows doubly exponentially in k, and so does the smallest number that never appears as a denominator in such a sum. OpenAI published a Lean proof, about 350 files and 44,000 lines, not counting Mathlib, and lists the main statements in its formalization catalog. We haven’t run the check.

2:44How the proof goes

Write S for log b. About log S greedy steps either finish, or leave a fraction A/C, with C in a chosen range. Then the proof builds a helper number M, a product of many primes, with lots of divisors. Here’s the key move. For a numerator u and a divisor t of M, one unit fraction peels off and leaves a new numerator: the remainder of −Qt modulo u, where Q is C or one. If some divisor makes that remainder small, the problem shrinks. Products of primes, chosen deterministically at large ranges and at random at small ones, make small remainders common. Descending through about log S ranges, some numerators fail. A uniform bound on the small divisors of numbers in a shifted interval, with Hölder’s inequality, keeps those failures from piling up. Almost every numerator in a long interval gets a short expansion. Finally, every numerator: a multiple, g·A·M, is the sum of two numerators from that almost-everything family. Add their expansions, divide by g, and A/C is done.

3:52Where it stands

This is a preprint, not peer reviewed, and we haven’t run the Lean check. The constant in front of log log b isn’t computed, and the denominators may be huge: unlike Tenenbaum and Yokota’s bounds, nothing here controls their size. Greedy can need giant denominators, and some fractions need about log log b terms. If the proof holds, a constant times log log b is always enough.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.