Combinatorics

Erdős 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

References

No one has attempted this yet.

Formal statement

Lean type

(∃ k > 2, Erdos835.Property k) ↔ True

What you must prove

import FormalConjectures.ErdosProblems.«835»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos835.erdos_835" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/835.lean

Source type SHA-256: sha256:f967e72c8bf53da5895721dfe2bcf951ec3b0ace3ff8180ca1355d1639d592a4
Task id: fc-379fc029-erdos835-erdos-835-9e8d3324fd-formalized-v1
Task commitment: sha256:c3835c97edc7fa330f6da6e024f1345684b793d4b3471b9abd211659c0cf3f88

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.