---

Claim. Let $F(k)$ be the number of $k$-element sets of positive integers whose reciprocals sum to $1$, each counted once (the increasing $k$-tuples $1\le n_1<\cdots<n_k$ with $1/n_1+\cdots+1/n_k=1$). The manuscript Short Egyptian fractions of the OpenAI mathematics release (OpenAI, 25 September 2026; the release attributes it to an internal OpenAI model and names no individual author, and its README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification) states as its Corollary 1.2 that there are absolute constants $c,C>0$ and $k_0$ with

$$ck\ \le\ \log\log F(k)\ \le\ Ck \qquad\text{for every } k\ge k_0 ,$$

that is, $F(k)=\exp(\exp(\Theta(k)))$. The lower half is the new content: it removes the $1/\log k$ from the recorded lower bound $\exp(\exp(ck/\log k))$ of Konyagin and of Elsholtz. The upper half was known, and the manuscript's own explicit bound $F(k)\le k^{2^k-1}$ is weaker than the Elsholtz–Planitzer bound the problem page records. The constants are not made explicit. The route: the manuscript's Theorem 1.1 (the accepted claim of Problem 304) applied to $(Q-1)/Q$, for $Q$ the product of the first $r$ odd primes, gives a distinct expansion of $1$ of length $O(\log r)$ containing a denominator with at least $2^r$ divisors; splitting that denominator over its proper divisors gives about $2^r$ distinct expansions of one length, and an injective padding of the largest denominator reaches 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 is recorded there at the level of its structure, with its steps unverified.

Depends on. The release's Theorem 1.1 supplies the short expansion of $(Q-1)/Q$; in the Lean development counting_double_log_order is proved from main_double_log_order, the declaration that page records.

Covers. The double-exponential order of $F(k)$, the number of $k$-element sets of positive integers with reciprocal sum $1$: there are $c,C>0$ with $ck\le\log\log F(k)\le Ck$ for all large $k$, so $F(k)=\exp(\exp(\Theta(k)))$. This replaces the recorded lower bound $\exp(\exp(c'k/\log k))$; the upper half was already known (Elsholtz–Planitzer). Not settled: an asymptotic formula, $F(k)$ up to constant factors, or the constant in $\log\log F(k)$ (the monograph's guess $c_0^{2^{k(1-\varepsilon)}}$).

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.counting_double_log_order, which states $ck\le\log\log F(k)\le Ck$ with the quantifiers $\exists c,C>0\ \exists k_0\ \forall k\ge k_0$, and the theorem OAI.Problem337.one_expansions_finite_and_bounded, which proves for every $k$ that the set of expansions is finite with $F(k)\le k^{2^k-1}$ and that every denominator of a $k$-term expansion of $1$ satisfies $n_i\le k^{2^{i-1}}$. Here OneExpansions k is the set of strictly increasing tuples Fin k → ℕ with entries at least $1$ and reciprocal sum exactly $1$, which correspond one to one with the $k$-element sets the problem counts, and F k is its ncard; the finiteness statement excludes the junk value $0$ of ncard on an infinite set, and the lower bound $ck\le\log\log F(k)$ with $ck>0$ excludes it a second time since Real.log 0 = 0. 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 internal label and is unrelated to catalog Problem 337.

The claim is partial because the problem asks for good estimates and the declaration fixes only the order of the double logarithm: no asymptotic formula, no estimate of $F(k)$ up to constant factors and no value of the constant in $\log\log F(k)$ (the monograph's guess $c_0^{2^{k(1-\varepsilon)}}$ would mean a slope tending to $\log2$) follows from it. No other acceptance evidence was found on 2026-10-07: the manuscript was not refereed and had no arXiv version, no outside review of it was recorded, and the site's page showed the label OPEN (last edited 27 September 2025) with no proof claim on its tab on 2026-10-07.