Erdős problem 564

Let $R_3(n)$ be the minimal $m$ such that if the edges of the $3$ -uniform hypergraph on $m$ vertices are $2$ -coloured then there is a monochromatic copy of the complete $3$ -uniform hypergraph on $n$ vertices.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

564.lean

Retained formal statement1 of 1

Let $R_3(n)$ be the minimal $m$ such that if the edges of the $3$ -uniform hypergraph on $m$ vertices are $2$ -coloured then there is a monochromatic copy of the complete $3$ -uniform hypergraph on $n$ vertices.

Is there some constant $c>0$ such that $R_3(n) \geq 2^{2^{cn}}?$

FormalConjectures/ErdosProblems/564.leanErdos564.erdos_5641 lineExact file

1True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ 2 ^ (c * n) ≤ ↑(Combinatorics.hypergraphRamsey 3 n)

OpenStatement only, no proof