---

Claim. For $k\ge1$ let $D_k$ be the set of integers $m\ge2$ that occur as a denominator in some representation $1=1/n_1+\cdots+1/n_k$ with $1\le n_1<\cdots<n_k$, and let $v(k)=\min\{m>1:m\notin D_k\}$, as in the problem page's corrected Statement. The manuscript Short Egyptian fractions of the OpenAI mathematics release (OpenAI, 25 September 2026; the release's README says that its manuscripts were produced by an internal OpenAI model and that the collection includes results at different stages of verification, and it names no individual author) states as its Corollary 1.3 that for every sufficiently large $k$

$$e^{e^{k/600}}\ \le\ v(k)\ \le\ 1+k^{2^{k-1}}, \qquad \frac{\log2}{257}\le\liminf_{k\to\infty}\frac{\log\log v(k)}{k} \le\limsup_{k\to\infty}\frac{\log\log v(k)}{k}\le\log2 ,$$

and that for each fixed $c<\log2/257$, $v(k)\ge e^{e^{ck}}$ for all large $k$. So $\log\log v(k)=\Theta(k)$. The lower bound is the new content: it proves the doubly exponential growth that van Doorn and Tang's Section 3 anticipated from the conjecture of Problem 304, and it rules out the monograph's alternative guess $2^{2^{\sqrt k}}$. The upper bound is weaker than the recorded $c_0^{(2/5+o(1))2^k}$, as the manuscript says. The route: a greedy prefix that reserves the denominator $m$ reduces to a remainder to which the manuscript's Theorem 1.1 (the accepted claim of Problem 304) applies, giving a distinct expansion of $1$ containing $1/m$ of length $O(\log\log m)$; a separate construction with an explicit coefficient gives length at most $(257/\log2+\varepsilon)\log\log m$ for large $m$; a padding that preserves one denominator (van Doorn and Tang's Lemma 2.1, reproved) carries each marker to every larger length. 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; the prose proof was read there for structure only and no step was checked.

Depends on. The release's Theorem 1.1, in the manuscript's proof of the corollary, supplies a marked expansion of $1$ through $1/m$ only for the finitely many small $m$ below the threshold of the explicit construction; the slope $\log2/257$ comes from that construction (the manuscript's Proposition 8.1), not from Theorem 1.1. The Lean proof does not use that theorem at all: at the pinned revision prescribed_denominator_corollary is assembled in Main.lean from exact_marker_padding, every_exact_marker_occurs, quantitative_marked_length and missing_denominator_semantics, and every_exact_marker_occurs is an elementary telescoping construction in MarkerOccurrence.lean (the reciprocal of $m$ plus reciprocals of pronic numbers), while main_double_log_order, the declaration that page records, enters only the separate counting theorem counting_double_log_order. The formalized evidence therefore stands on its own; the link records the prose proof's use of the accepted theorem.

Covers. The double-exponential order of $v(k)$ (the problem page's corrected Statement: least $m>1$ in no $k$-term representation of $1$). For all large $k$, $e^{e^{k/600}}\le v(k)\le1+k^{2^{k-1}}$, and $\log2/257\le\liminf\log\log v(k)/k\le\limsup\log\log v(k)/k\le\log2$; for each $c<\log2/257$, $v(k)\ge e^{e^{ck}}$ eventually. So $\log\log v(k)=\Theta(k)$. This proves the $e^{e^{ck}}$ lower bound van Doorn–Tang anticipated and rules out the monograph's $2^{2^{\sqrt k}}$ alternative. Not settled: the exact slope (whether $\log\log v(k)/k\to\log2$, the monograph's $2^{2^{k(1-\varepsilon)}}$ guess) or any asymptotic for $v(k)$.

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.prescribed_denominator_corollary, whose three conjuncts are the displayed bounds for all $k\ge k_0$, the liminf and limsup inequalities for prescribedSlope k, which is $\log\log v(k)/k$, and the bound $e^{e^{ck}}\le v(k)$ eventually for every $c<\log2/257$, and the theorem OAI.Problem337.missing_denominator_semantics, which proves for every $k$ that D k is finite, that the missing set is nonempty, that v k is at least $2$, lies outside D k and is the least such integer, and that $v(k)\le1+k^{2^{k-1}}$ for $k\ge1$; so v k is the attained minimum of the Formulation's set and not the junk value of an empty infimum, and the real liminf and limsup are not their default $0$ because $\log2/257>0$ bounds them below. The definitions (IsOneExpansion: denominators at least $1$, strictly increasing on Fin k, exact sum $1$; D, which collects denominators at least $2$; missingDenominators; v) are the Formulation's $D_k$ and $v(k)$, the omission of $1$ from D being harmless since $v$ looks only at $m>1$. 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 and does not refer to catalog Problem 337. The same comparator holds OAI.Problem337.exact_marker_padding, the nesting $D_r\subseteq D_{r+1}$ for $r\ge3$.

The claim is partial because the problem asks to estimate the growth and the declaration fixes only the double-logarithmic order, with the slope pinned to $[\log2/257,\log2]$: whether $\log\log v(k)/k\to\log2$ (the monograph's $2^{2^{k(1-\varepsilon)}}$ guess) and any asymptotic for $v(k)$ are open. The threshold $k_0$ is existential, so the bound is ineffective and does not replace van Doorn and Tang's $v(k)\ge e^{ck^2}$ for every $k\ge1$ (their claim page) on the small range. 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 as read on 2026-10-07.