---

Claim. With $n_k$ as in Problem 1063, the README of the repository pw/erdos1063-upper-bound states as its Theorem that there is an absolute constant $C$ with

$$n_k\le\exp\Bigl(C\,\frac{k\log\log k}{\log k}\Bigr)$$

for all sufficiently large $k$, so that $n_k=\exp(o(k))=o(k\,[1,\ldots,k-1])$. The proof is an explicit construction of $n$ through $p$-adic valuation and carry conditions, with one simultaneous Dirichlet pigeonhole step. The README is signed by Patrick White and Claude (MathDyad). It says that GPT-5.6 Sol produced the construction through Codex, that Claude re-verified it with a checker written from scratch over 17 values of $k$ from 4 to 300, that no human mathematician has reviewed it, and that it was not posted to the site's forum. The README says that it does not claim to solve the problem. The formal-conjectures catalog's docstring for erdos_1063.variants.subexponential_upper_bound cites the repository as an earlier proposed bound.

Covers. The upper bound above. It is weaker than the bound claimed on Cipollini's page and the one proved in the Lean file on the LEAP page. Not covered: any lower bound, the order of $\log n_k$, and the estimate Erdős and Selfridge asked for.

Standing. Claimed. There is no refereed version, no site acceptance and no outside review; the site labels the problem OPEN.

Depends on. No page of this wiki.