---

Claim. With $c_0=14/\log2\approx20.2$, for every sufficiently large $k$ every integer $b$ with $2\le b\le\exp\exp\sqrt{k/(2c_0)}$ occurs as a denominator in some representation $1=1/n_1+\cdots+1/n_k$ with $1\le n_1<\cdots<n_k$, so that

$$v(k)\ \ge\ \exp\Bigl(\exp\Bigl(\sqrt{k/(2c_0)}\Bigr)\Bigr)$$

for all large $k$. This is Theorem 1.3 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 first question the note's Theorem 1.1 answers (its claim page); the tab of Problem 293 carries no entry for it. The route: the note's Proposition 4.1 gives, for every large $x$ and a prescribed odd prime $p_*$, a practical $n\in[x,x^2)$ with $p_*\nmid n$ and $h(n)\le c_0(\log\log x)^2-1$; its Lemma 5.1 writes $(b-1)/b$ as at most $2h(n)$ distinct unit fractions none equal to $1/b$, taking $n$ with $b\le n<b^2$ and $b\nmid n$; adjoining $1/b$ gives a decomposition of $1$ containing $b$ with fewer than $2c_0(\log\log b)^2\le k$ terms, and van Doorn and Tang's nesting lemma ($D_r\subseteq D_{r+1}$) pads it to exactly $k$ terms. The note says it is 80 to 90 percent AI-generated: ChatGPT simplified the argument behind Price's bound for Problem 18 and adapted it to the applications, 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 lower bound $v(k)\ge\exp\exp\sqrt{k/(2c_0)}$ for all large $k$, doubly exponential in $\sqrt k$; nothing on the upper side. For large $k$ it lies between van Doorn and Tang's refereed $e^{ck^2}$ (their claim page) and the OpenAI release's accepted $e^{e^{k/600}}$ (its claim page), which implies it; the problem page does not adopt it into the recorded bounds.

Depends on. No page of this wiki; the proof uses the note's own Lemma 5.1 and Proposition 4.1 and the nesting lemma of van Doorn and Tang, which is recorded on the library card of their paper.

Formalization by the authors. The repository's Lean file, linked above at the same commit, imports Mathlib, declares Lean v4.28.0, contains no sorry and ends with #print axioms commands for its three main theorems. Its SDS.exists_egyptian_with_prescribed_denominator states that for all large $k$ and all $2\le b\le\exp\exp\sqrt{k/(2c_0)}$ there is a $k$-element set $A$ of positive integers containing $b$ with $\sum_{d\in A}1/d=1$, which is Theorem 1.3. It is not stated against any formal-conjectures declaration (none exists for this problem). This corpus has not built the file, so no formalized evidence is listed.

Standing. The claim is claimed. The note is not on arXiv and not refereed, no independent reviewer is documented, the site shows the problem OPEN with no proof claim on its own tab, and the proof claim on Problem 18's tab, labeled partial when read, is not accepted.