---

Claim. With $c_0=14/\log2\approx20.2$, there are infinitely many practical $n$ with

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

where $h(n)$ is the least number of distinct divisors of $n$ that always suffice to write every positive integer below $n$ as a sum. This is Theorem 1.1 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 on the problem's proof-claims tab as a partial proof. It answers the first question of Problem 18, the question carrying the prize, in the affirmative with an explicit constant. The construction extends a practical number $n$ by a modulus $A$: when every residue modulo $A$ is a sum of at most $L$ distinct divisors of $n$, none divisible by $A$ and of total at most $n$, the product $An$ is practical with $h(An)\le h(n)+L$. An elementary criterion (the note's Lemma 3.2, proved by Cauchy–Schwarz, Plancherel and character orthogonality on the divisor sets) and an averaging argument over random sets of primes (Lemma 3.3, with the prime number theorem and Hölder's inequality) find such a squarefree odd $A$ with $L=4$ (Corollary 3.4) and a prescribed number of prime factors. The note presents its result as a simplified and explicit version of Price's claim and does not mention Bourgain. In this page's comparison, the two lemmas take the place of the exponential-sum theorem of Bourgain that, according to the comment of 6 August 2026 on that claim, Price's argument uses. Iterating the extension gives Proposition 4.1, a practical $n\in[x,x^2)$ with $h(n)\le c_0(\log\log x)^2-1$ for every large $x$, with side conditions on the power of two and on a prescribed odd prime that serve the note's applications to Problem 304 and Problem 293; those applications are claims about other problems and are not recorded here. The note states 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 first question only: infinitely many practical $n$ with $h(n)<(\log\log n)^{O(1)}$, here with exponent $2$ and an explicit constant. The claim says nothing about $h(n!)$, so the second and third questions are untouched.

Depends on. No page of this wiki.

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.infinitely_many_divisor_representable states that for every $N$ there is $n>N$ such that every $1\le m\le n$ is the sum of a set of at most $c_0(\log\log n)^2$ divisors of $n$. It is not stated against the catalog's Erdos18.erdos_18a, whose right side it implies with $C=3$ through two elementary steps not formalized anywhere: that such an $n$ is practical, and that $c_0(\log\log n)^2<(\log\log n)^3$ once $n>\exp\exp c_0$. This corpus has not built the file, so no formalized evidence is listed.

Standing. The claim is claimed. The site labeled the claim partial and shows the problem open (by 2026-10-07 its proof-claims tab listed all three claims as "A proof claimed by"), its curator has not accepted it, the note is not on arXiv and not refereed, and no independent reviewer is documented.