---

Claim. For integers $1\le a<b$ let $N(a,b)$ be the least number of distinct unit fractions with denominators above $1$ whose sum is $a/b$, and $N(b)=\max_{1\le a<b}N(a,b)$, the extremal function of Problem 304. With $c_0=14/\log2$, for every sufficiently large $b$,

$$N(b)\le2c_0(\log\log b)^2 .$$

This is Theorem 1.2 of the note "Practical numbers and Egyptian fractions" by Wouter van Doorn and GPT-6 Astra Pro (the author line as printed), posted on 16 September 2026 in the GitHub repository linked above at its pinned commit and registered the same day as a partial proof claim on the proof-claims tab of Problem 18, whose claim summary states this bound for Problem 304 beside the note's main result. The route: the note's Lemma 5.1 writes $an=bq+r$ for a practical $n\ge b$ and represents $q$ and $r$ as sums of at most $h(n)$ distinct divisors of $n$ each, so that $a/b$ is a sum of at most $2h(n)$ distinct unit fractions; its Proposition 4.1 supplies a practical $n\in[b,b^2)$ with $h(n)\le c_0(\log\log b)^2-1$. The note says that it is 80 to 90 percent AI-generated: ChatGPT simplified and adapted the argument, Aristotle formalized the proofs, and the human author edited the opening and closing sections. The human author is the claimant here; the card is doorn_2026_practical_numbers_egyptian_fractions.

Submission note. Posted to erdosproblems.com as a proof claim by Wouter van Doorn (account Woett) on 16 September 2026, giving "GPT-6 Astra Pro" as the AI used:

As mentioned in the comments to the proof claim by Liam, bounds on $h$ can provide bounds on $N(b)$ from #304, which can in turn give bounds on $v(k)$ from #293. The linked (mostly AI-generated) write-up does exactly that: it proves a version of $h(n) \ll (\log \log n)^2$ which contains a few extra hypotheses on $n$, in order to be able to use this $n$ in #304 and #293 as well. As a bonus this proof is explicit and, with $c_0 = \frac{14}{\log 2} \approx 20.2$, gives infinitely many $n$ with

$$> h(n) \le c_0 (\log \log n)^2, >$$

while

$$> N(b) \le 2c_0(\log \log b)^2 \qquad \text{and} \qquad v(k) \ge e^{e^{\sqrt{\frac{k}{2c_0}}}} >$$

hold for all sufficiently large $b$ and $k$ respectively. Perhaps more importantly, as a further bonus the proof is a bit more elementary, which made it surprisingly easy to fully formalize all these results on $h(n), N(b)$ and $v(k)$. Notes: In the Lean file, the three main results can all be found at the very end. Apart from the definition of $c_0 = \frac{14}{\log 2}$, these three statements are fully self-contained and do not use any other notation or definitions.

Covers. The upper bound $N(b)\le2c_0(\log\log b)^2$ for all large $b$ only. It does not settle the problem's question, whether $N(b)\ll\log\log b$, which the OpenAI release's accepted claim answers; it would replace Vose's bound $N(b)\ll\sqrt{\log b}$ if correct, and the accepted bound implies it.

Depends on. The note's Theorem 1.1 and Proposition 4.1 on Problem 18: the bound is an application of the same construction, and it stands or falls with that pending claim.

Formalization by the authors. The repository's Lean file, linked above at the same commit, states the bound as SDS.exists_short_egyptian_fraction: for every large $b$ and every $1\le a<b$ there is a finite set $A$ of positive integers with at most $2c_0(\log\log b)^2$ elements whose reciprocals sum to $a/b$; a Finset has distinct elements, and $1\notin A$ since $a/b<1$, so the statement is the theorem as printed. The file contains no sorry and ends with #print axioms commands for its three main theorems. This corpus has not built the file, so no formalized evidence is listed.

Standing. Claimed. The claim is registered on Problem 18's tab, not on this problem's, whose tab is empty; the site labels Problem 304 OPEN (page last edited 29 December 2025) and its curator has not accepted the note, which is not on arXiv and not refereed, and no independent reviewer is documented.