Erdős Problem 835 and the Middle Johnson Graph:
A Verified Reduction, a Primality Sieve, and Machine-Checked Small Cases

1. The statement and its reduction

Write \([m]=\{1,\dots,m\}\). For a fixed \(k\), colour each \(k\)-subset of \([2k]\).

Two \(k\)-subsets \(S,T\) lie in a common \((k+1)\)-set iff \(|S\cap T|=k-1\) iff \(|S\triangle T|=2\) — exactly adjacency in the Johnson graph \(J(2k,k)\). The \(k\)-subsets of a fixed \((k+1)\)-set \(A\) form a clique of size \(k+1\) (an "anti-star"), and every edge of \(J(2k,k)\) lies in such a clique (namely \(A=S\cup T\)). Hence "all \(k+1\) colours on every anti-star clique" is equivalent to a proper \((k+1)\)-colouring of \(J(2k,k)\): properness forces each \((k+1)\)-clique to be rainbow, and rainbow-on-all-anti-stars forces properness on every edge. This is the standard reduction:

Because each anti-star clique has size \(k+1\), always \(\chi(J(2k,k))\ge k+1\); the question is whether the chromatic number meets this clique lower bound.

2. The exact packing bound: colour classes are Steiner systems

A colour class is a set of \(k\)-subsets, no two adjacent in \(J(2k,k)\): an independent set, equivalently a binary constant-weight code of length \(2k\), weight \(k\), minimum Hamming distance \(\ge 4\). Two weight-\(k\) words at distance \(2\) share \(k-1\) ones, so distance \(\ge 4\) forbids any \((k-1)\)-subset lying in two codewords. Each codeword (a \(k\)-set) contains \(\binom{k}{k-1}=k\) of the \(\binom{2k}{k-1}\) many \((k-1)\)-subsets, so a class has at most

codewords — the \(k\)-th Catalan number — with equality iff every \((k-1)\)-subset is covered exactly once, i.e. iff the class is a Steiner system \(S(k-1,k,2k)\). Since a colouring partitions all \(\binom{2k}{k}\) vertices into \(k+1\) classes and \((k+1)C_k=\binom{2k}{k}\) exactly, a proper \((k+1)\)-colouring forces every class to attain the bound. This proves the sharp characterization.

In particular, if the Steiner system \(S(k-1,k,2k)\) does not exist then \(A(2k,4,k)\le C_k-1\), and

the last equality verified exactly for every tested \(k\) (script sieve_835.py). One missing codeword is already enough to jump from the clique bound \(k+1\) to \(k+2\) — the value in the strengthened open conjecture \(\chi(J(2k,k))\ge k+2\).

3. A primality sieve for the Steiner system

The Steiner system \(S(t,K,v)\) with \(t=k-1\), \(K=k\), \(v=2k\) exists only if, for every \(0\le i\le t\), the count \(\lambda_i=\binom{v-i}{t-i}\big/\binom{K-i}{t-i}\) is a positive integer. Here \(\binom{K-i}{t-i}=\binom{k-i}{1}=k-i\), so the conditions read

The index \(i=k-2\) gives \(\lambda_{k-2}=\binom{k+2}{1}/\binom{2}{1}=(k+2)/2\), an integer iff \(k\) is even. Thus every odd \(k>2\) fails immediately (a one-line obstruction). Exact integer computation over the full range yields the clean statement:

The sieve reports zero mismatches against primality over \(2\le k\le 300\), and the surviving parameters are exactly \(k+1\in\{3,5,7,11,13,17,19,23,\dots\}\). A worked sample of the failing design equations:

Independent corroboration. The recursive Johnson bound \(\mathrm{jb}(2k,4,k)\) formalised in the 835 entry satisfies \(\mathrm{jb}(2k,4,k)=C_k\) exactly when \(k+1\) is prime and is strictly smaller otherwise (script johnson_bound_835.py, \(3\le k\le 60\)). Two entirely different computations — design divisibility and the code-size recursion — isolate the identical hard core \(\{k:\,k+1\text{ prime}\}\).

4. Machine-checked small cases

For a fixed \(k\) the decision "\(\chi(J(2k,k))\le k+1\)?" is finite. We settle it with independent oracles that must agree: a self-contained exhaustive backtracking prover (MRV + forward checking, with a sound symmetry break fixing one \((k+1)\)-clique to the identity colouring, and again with no symmetry break at all), cross-checked against CaDiCaL, Glucose 4, and MiniSat 2.2 (scripts settle_835.py, crosscheck_nosym.py; DIMACS CNF emitted for third-party replay). For a YES we independently re-verify that the returned colouring is proper and makes every \((k+1)\)-subset rainbow.

\(k=2\) (YES). The three antipodal pairs of disjoint \(2\)-subsets \(\{12,34\},\{13,24\},\{14,23\}\) are the three colour classes: a \(1\)-factorization of \(K_4\), equivalently the large set \(LS[3](1,2,4)\). Each \(3\)-subset meets all three pairs, hence is rainbow.

\(k=3\) (NO). \(S(2,3,6)\) is a Steiner triple system on \(6\) points, which does not exist (\(v\equiv1,3\pmod 6\) fails at \(6\)); equivalently \(\lambda_1=5/2\). Independently, \(J(6,3)\) is not \(4\)-colourable — confirmed by exhaustive search (\(9\) nodes with the symmetry break, \(257\) without) and by all three SAT solvers.

\(k=4\) (NO) — the first structural case. Here \(k+1=5\) is prime and the Steiner system \(S(3,4,8)\) (the Steiner quadruple system \(\mathrm{SQS}(8)\), \(14\) blocks) does exist, so Theorem 2 cannot decide it: the obstruction is that no large set of five disjoint \(\mathrm{SQS}(8)\) tiles the \(70\) quadruples. We prove \(\chi(J(8,4))=6\) directly. Five independent oracles agree the \(70\)-vertex graph is not \(5\)-colourable: our exhaustive prover closes the whole tree in \(136\) nodes with the clique symmetry break and in \(11\,486\) nodes (\(0.46\)s) with a DSATUR search using no symmetry assumption whatsoever, and CaDiCaL, Glucose, and MiniSat each return UNSAT on the emitted CNF (\(350\) variables, \(3575\) clauses).

\(k=5\) (NO). \(S(4,5,10)\) fails divisibility (\(\lambda_2=\binom{8}{2}/3=28/3\)); no Steiner system, so \(\chi(J(10,5))\ge 7\).

\(k=6\) (NO) — the case Erdős and Rosenfeld were unsure about. Here \(k+1=7\) is prime and \(S(5,6,12)\) exists, so — as at \(k=4\) — the obstruction is at the large-set level. We settle it directly: CaDiCaL proves the \(924\)-vertex, \(7\)-colour instance \(J(12,6)\) UNSAT in \(328\) s (with one anti-star clique fixed to the identity colouring), so \(\chi(J(12,6))>7\) and \(835(6)\) is NO — an independent confirmation of Brouwer's tabulated value rather than a citation of it.

5. The frontier

Combining the above with [MT25]: \(835(k)\) is NO for every \(k>2\) with \(k+1\) composite (Theorem 2, independently of [MT25]), and for \(k+1\) prime it is NO whenever either the Steiner system \(S(k-1,k,2k)\) fails to exist (so \(A(2k,4,k)

python -m pip install python-sat sympy
python sieve_835.py            # Theorem 2 sieve (2..300), strict-gap check, survivors = {k+1 prime}
python settle_835.py 2 3 4     # own prover + CaDiCaL/Glucose/MiniSat, DIMACS emitted, witnesses verified
python crosscheck_nosym.py 2 3 4   # independent full search, NO symmetry break
python johnson_bound_835.py    # recursive Johnson bound; hard core = {k+1 prime}, 3..60