Claims

../

2025_12_31_ma_tang: Ma and Tang's note proves that the Johnson graph J(2k,k) has chromatic number greater than k + 1 whenever k > 2 and k + 1 is not prime, so no coloring of the kind asked for exists for those k; a partial no.

2026_01_23_deepmind: A Lean proof found by AlphaProof that the Johnson graph J(18,9) does not have chromatic number 10, so the case k = 9 of the question has answer no; posted in a formal-conjectures pull request and removed before the merge.

---