{"id":"palomar/PALOMAR-2026-11-01-000008","url":"https://github.com/stokes/erdos835-palomar/tree/3a8d4cb348203b172c050917eaf1fa03679f002f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000008-v1.json","repo":"https://github.com/stokes/erdos835-palomar","tags":["math.CO","msc:05C15","msc:05D05"],"score":0,"title":"Erdős Problem 835 when k + 1 is composite: the chromatic number of J(2k, k) exceeds k + 1","trust":"high","domain":"math.CO","source":"palomar","authors":["Matt Stokes"],"reviews":0,"subject":"math.CO","summary":"Erdős Problem 835 asks whether, for some k > 2, the k-element subsets of a 2k-element set can be coloured with k + 1 colours so that every (k + 1)-element set sees all k + 1 colours among its k-element subsets; equivalently, whether the Johnson graph J(2k, k) has chromatic number k + 1 for some k > 2. Jie Ma and Quanyu Tang showed that this fails whenever k + 1 is not prime. This Lean 4 formalization proves, with Mathlib only: the equivalence between the colouring property and χ(J(2k, k)) = k + 1 for k > 0; χ(J(2k, k)) > k + 1 for every k > 2 with k + 1 composite; the consequence for every…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"A note on Erdős Problem #835","identifier":"https://github.com/QuanyuTang/erdos-problem-835/blob/main/On_Problem_835.pdf","relationship":"formalizes"}]}