---

Claim. $\chi(J(18,9))\ne 10$: the $9$-subsets of $\{1,\ldots,18\}$ have no coloring with $10$ colors in which every $10$-subset sees all $10$ colors, so the case $k=9$ of Problem 835 has answer no. The proof is the theorem johnsonGraph_18_9_chromaticNumber in the formal-conjectures statement file for the problem at the first commit linked above, of 23 January 2026. A comment in the site's discussion thread on 26 January 2026, by the author of the pull request carrying the commits, reports that AlphaProof found the proof on 26 December 2025, when the file still listed the case as open. The second commit, of the same day, adapts the proof to every odd $k\ge 11$ (johnsonGraph_chromaticNumber, for $k=l+3$ with $l>6$ even); the comment calls that adaptation human work, so this page credits AlphaProof with the case $k=9$ only and records the adaptation without crediting it. Both proofs were removed in a later commit of the same pull request, before it was merged on 26 January 2026, and the merged file states the case $k=9$ with a sorry body.

Submission note. Posted to the site's forum by Yaël Dillies on 26 January 2026:

AlphaProof (on 2025-12-26) found a proof that $J(18, 9) \ne 10$, which was the first result we marked as open in formal-conjectures (albeit it was in fact not, see below).

Then we realised this proof could easily be adapted to work for all odd $k$ (on 2025-12-27) and Lean agreed. We even thought it could be generalised to all $k$ such that $k + 1$ is composite, but did not pursue this further as we simultaneously realised that Johnson's bound along with the independence bound on the chromatic number of a graph gives the same value (or even better sometimes).

Concretely, Johnson proved that the independence number of $J(n, k)$ is at most $A(n, 4, k)$, which is recursively defined by $A(n, 4, 1) = 1$ and $A(n, 4, k) = \lfloor \frac nk A(n - 1, 4, k - 1)\rfloor$ for $k > 1$. The lower bound on the chromatic number is then $\lceil \binom{2k}k/ A(2k, 4, k)\rceil$, which is at least $k + 2$ precisely when $k + 1$ is composite.

We thought to mention here that the result is in fact not novel, although it does indeed seem no one in the coding theory literature bothered to evaluate $A(2k, 4, k)$ in relation to this problem.

The original Alphaproof proof is here, the human-powered generalisation is there, and the current state of the formal proof is in this PR to formal-conjectures .

Covers. The case $k=9$: the answer is no. Not covered: every other $k$. The case lies inside the composite-$(k+1)$ result of Ma and Tang, since $k+1=10$, and the comment itself says the result is not new: Johnson's bound on the independence number of $J(2k,k)$, with the bound $\chi\ge|V|/\alpha$ on the chromatic number, gives $\chi(J(2k,k))\ge k+2$ exactly when $k+1$ is composite.

Depends on. No page of this wiki.

Acceptance. None recorded. The site's commentary does not mention the proof, and the site labels the problem VERIFIABLE, an open label. The Lean proof is attributed to AlphaProof, as the comment names it. This corpus has not built the file at either commit or audited the theorem's statement, so the links are not formalized evidence; nothing on this page is this project's own review.