---

Claim. For integers $1\le a<b$ let $N(a,b)$ be the least $k$ for which $a/b=1/n_1+\cdots+1/n_k$ with integers $1<n_1<\cdots<n_k$, and let $N(b)=\max_{1\le a<b}N(a,b)$, the maximum over every numerator with no coprimality condition. The manuscript Short Egyptian fractions of the OpenAI mathematics release (OpenAI, 25 September 2026) states as its Theorem 1.1 that there are absolute constants $c_1,c_2>0$ and $b_0$ with

$$c_1\log\log b\ \le\ N(b)\ \le\ c_2\log\log b \qquad\text{for every } b\ge b_0 .$$

The upper half answers the problem's question: $N(b)\ll\log\log b$, the finitely many $b<b_0$ being absorbed into the constant. With the lower half, which is Erdős's bound of 1950 (Theorem 2 of that paper, for the numerator $b-1$, the accepted partial claim Erdős's 1950 bounds) reproved in the manuscript, $N(b)\asymp\log\log b$, which is also the order of magnitude that the problem's request to estimate $N(b)$ asks for. The constants $c_1,c_2,b_0$ are not made explicit. The manuscript's method is a descent: a greedy prefix reduces $a/b$ to a remainder over a large denominator $C$, an auxiliary integer $M$ built from products of primes near a power of $\log b$ is chosen so that almost every numerator over $MC$ has an expansion of length $O(\log\log b)$, and the remainder's numerator is split into two such good numerators; the exceptional numerators are controlled by a uniform moment bound for a truncated divisor function. The statement, its locators and a structural reading of the proof are on the result page of the source card, whose card records the release's provenance and attestations; no step of the prose proof is checked here. The release's README says that its manuscripts and supporting proof artifacts were produced by an internal OpenAI model and that the collection includes results at different stages of verification, not all with Lean formalizations; it names no individual author.

Acceptance. The evidence is formalized. The release's Lean development at the pinned revision declares, in lean/OAI/NumberTheory/EgyptianFractions/Main.lean, the theorem OAI.Problem337.main_double_log_order, which states the two-sided bound for maxEgyptianLength b (the maximum over Finset.range b of the least length of an expansion of $a/b$, the slot $a=0$ zeroed) with the quantifiers $\exists c_1,c_2>0\ \exists b_0\ \forall b\ge b_0$, and the theorem OAI.Problem337.egyptian_length_is_minimum, which pins egyptianLength a b as an attained minimum for every $1\le a<b$ and so excludes the junk value of an empty infimum. The definitions (IsEgyptianExpansion: denominators at least $2$, strictly increasing on Fin k, exact rational sum, no cap on the denominators; egyptianLength; maxEgyptianLength) are the problem's $N(a,b)$ and $N(b)$. The corpus's verification built both declarations and checked their axioms, which are propext, Classical.choice and Quot.sound only, and the comparator challenge lean/ComparatorChallenges/EgyptianFractions.lean of the release pins these statements and definitions, with which the solution module's fingerprints were identical. The namespace Problem337 is the release's own label; it does not refer to catalog Problem 337, an unrelated additive-bases problem. The release holds a second, independent development of the same theorem, OAI.ShortEgyptian.main under lean/OAI/NumberTheory/ShortEgyptian/ with its own comparator challenge ShortEgyptianFractions.lean, stating existence of an expansion for every $a/b$ together with the two-sided bound; it is not part of the verification record and was not built here.

No other acceptance evidence exists: the manuscript is not refereed and has no arXiv version, no outside reviewer has examined it, and the site's page shows the label OPEN (last edited 29 December 2025) with no proof claim on its tab. The community database and the formal-conjectures statement file are recorded on the problem page.