Erdős Problem 562

Reference: erdosproblems.com/562

theorem Erdos562.erdos_562 : sorry ↔ ∀ r ≥ 3, Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) fun (n : ℕ) => ↑n

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.