Erdős problem 562

Let $R_r(n)$ denote the $r$ -uniform hypergraph Ramsey number: the minimal $m$ such that if we $2$ -colour all edges of the complete $r$ -uniform hypergraph on $m$ vertices then there must be some monochromatic copy of the complete $r$ -uniform hypergraph on $n$ vertices.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

562.lean

Retained formal statement1 of 1

Let $R_r(n)$ denote the $r$ -uniform hypergraph Ramsey number: the minimal $m$ such that if we $2$ -colour all edges of the complete $r$ -uniform hypergraph on $m$ vertices then there must be some monochromatic copy of the complete $r$ -uniform hypergraph on $n$ vertices.

Prove that, for $r \ge 3$ , $\log_{r-1} R_r(n) \asymp_r n,$ where $\log_{r-1}$ denotes the $(r-1)$ -fold iterated logarithm.

FormalConjectures/ErdosProblems/562.leanErdos562.erdos_5621 lineExact file

1True ↔ ∀ r ≥ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑n

OpenStatement only, no proof