---

Claim. For a practical number $m$ let $h(m)$ be the least number of distinct divisors of $m$ that always suffice to write every positive integer below $m$ as a sum. The second question of Problem 18 has the answer yes: for every $\varepsilon>0$ there is $n_0$ with

$$h(n!)<n^{\varepsilon}\qquad\text{for all }n\ge n_0,$$

that is, $h(n!)<n^{o(1)}$. The proof is a Lean file of 14,043 lines with no import statement, submitted under the handle JenW1N to the bounty site Conjectures.io, which had published the problem's second question as the formal-conjectures declaration Erdos18.erdos_18b with its answer marker left to be filled. The file fills the marker as True, pins the target type by rfl, and closes the target by deriving the bound from a Fourier-decay property of product measures built from sets of odd integers on the cyclic groups $\mathbb Z/2^J$, which it proves in the same file; the reduction and the formal statement are recorded on the target page of its card. No write-up accompanies the proof, and the file names no author and declares no AI system.

Submission note. Posted to erdosproblems.com as a proof claim by conjectures.io (account TFBloom) on 27 September 2026, giving "Unknown" as the AI used:

This formalisation claims a proof that $h(n!)\leq n^{o(1)}$. Notes: This was posted on conjectures.io. I have not verified the proof yet, and do not claim that the formalisation is correct, nor have I looked into the proof at all. I am posting this here so that others are aware that this claim has been made, and we can discuss it here. This should also not be read as any kind of endorsement of the conjectures.io program - in my view it is using these problems, which it does not care about, for its own ends, without making any attempts to explain these proofs or engage with the mathematical community. It is also not transparent (e.g. of who is running these through the AI, how long for, and which AI).

Covers. The second question only, $h(n!)<n^{o(1)}$. The formal statement quantifies over every real $\varepsilon>0$ and all sufficiently large $n$, with the catalog's practicalH as $h$ under the fresh-set reading (a new set of divisors may be chosen for each target). It says nothing about the first question, general practical $m$ with $h(m)<(\log\log m)^{O(1)}$, or the third, $h(n!)<(\log n)^{O(1)}$.

Depends on. No page of this wiki.

Acceptance. The reviewed evidence is the certification by Conjectures.io: its Lean kernel verified the proof with the axioms propext, Quot.sound and Classical.choice permitted and no second kernel run; its review approved the record the same day under its policy v3, through two independent agent assessments of one model family, without a fresh Lean replay; the record was certified on 17 September 2026 and its bounty paid. Conjectures.io's check that the proof's source type matches the catalog's declaration, and the comparison of the target with the catalog file, are on the card. Beyond the bounty site there is no acceptance: no refereed publication exists, and erdosproblems.com shows the problem open. Its curator, Thomas Bloom, posted the record on the problem's proof-claims tab on 27 September 2026 (third link) as a partial proof Bloom had not verified, so that posting discloses the result and reviews nothing. This corpus has not built the file, so no formalized evidence is listed.