Erdős Problem 835 when k + 1 is composite: the chromatic number of J(2k, k) exceeds k + 1
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000008
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000008/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000008/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'