Erdős problem 835

Does there exist a $k>2$ such that the $k$ -sized subsets of {1,...,2k} can be coloured with $k+1$ colours such that for every $A\subset \{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$ -sized subsets of $A$ ?

Sources

The source's own material, retained exactly.

13 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

835.lean

Retained formal statement4 of 13

Does there exist a $k>2$ such that the $k$ -sized subsets of {1,...,2k} can be coloured with $k+1$ colours such that for every $A\subset \{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$ -sized subsets of $A$ ?

FormalConjectures/ErdosProblems/835.leanErdos835.erdos_8351 lineExact file

1(∃ k > 2, Erdos835.Property k) ↔ sorry

OpenStatement only, no proof