---

Claim. With $n_k$ as in Problem 1063,

$$n_k=O\Bigl(\exp\Bigl(\frac{k}{\log k}\bigl(\log\log k+\log\log\log k+\log2\bigr)\Bigr)\Bigr),$$

and this bound is $o(k\,[1,2,\ldots,k-1])$. This is the theorem erdos_1063.better_upper of the linked Lean 4 file (about 5,500 lines, with no sorry and no axiom). Linfeng Song committed the file to a fork of formal-conjectures on 1 October 2026 and proposed it the same day in pull request 6781, which credits the proof to the LEAP prover agent of Kung, Song and coauthors (arXiv:2606.03303). The same file proves the Erdős–Selfridge exception, $n_k\le k!$ and $n_k\le k[1,\ldots,k-1]$ for $k\ge3$, and $n_k\le e^{(1+o(1))k}$. The catalog merged the pull request on 7 October 2026. It added erdos_1063.variants.subexponential_upper_bound, tagged research solved, with this file as its formal proof, linked the same file for the four companion statements, and kept erdos_1063.better_upper open. The file does not present itself as a formalization of another claimant's write-up, so it is recorded as an independent proof. Its bound gives $\log n_k\le\frac{k}{\log k}(\log\log k+\log\log\log k+\log2)+O(1)$, which implies the bound claimed on Cipollini's page.

Covers. The upper bound above. Not covered: any lower bound beyond $2k$, the order of $\log n_k$, and the estimate Erdős and Selfridge asked for.

Standing. Claimed. The file is third-party Lean that this corpus has not built or audited, so formalized is not listed. The catalog's merge review is not a mathematical review. The site labels the problem OPEN.

Depends on. No page of this wiki.