Colour k-subsets of [2k] with k+1 colours so every (k+1)-set is rainbow: possible for k>2? (Erdős #835)

Does there exist a $k>2$ such that the $k$-element subsets of $\{1,\ldots,2k\}$ can be coloured with $k+1$ colours such that for every $A\subseteq\{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$, all $k+1$ colours appear among the $k$-element subsets of $A$? Since the $k+1$ distinct $k$-subsets of such an $A$ pairwise intersect in $k-1$ elements, this asks exactly whether the Johnson graph $J(2k,k)$ — vertices the $k$-subsets of a $2k$-set, edges between subsets meeting in $k-1$ elements — has chromatic number equal to $k+1$ for some $k>2$.

Acceptance. FULLY RESOLVES (yes direction): for some specific $k>2$, an explicit assignment of one of $k+1$ colours to each $k$-subset of $\{1,\ldots,2k\}$ together with a machine check that every $(k+1)$-subset sees all $k+1$ colours (equivalently, a proper $(k+1)$-colouring of $J(2k,k)$); fully machine-checkable. FULLY RESOLVES (no direction): a proof that $\chi(J(2k,k))>k+1$ for all $k>2$ — machine-checkable (Lean/Coq; the statement is formalized in the DeepMind formal-conjectures repository) preferred, else a complete written proof. ADVANCES: settle a new individual case beyond those stated in the background (known: $3\leq k\leq 8$ are no, and all $k$ not of the form $p-1$ are no) — e.g. determine whether $\chi(J(20,10))=11$ via a verified SAT/ILP computation with a reproducible encoding and, for a negative answer, an UNSAT certificate or a rigorously justified symmetry-reduced exhaustion; or extend the Ma–Tang exclusion to further families of $k$; or prove improved general bounds on $\chi(J(2k,k))$. Deliver the colouring file plus checker script, or the proof file, or the encoding plus certificates for the case settled.