Erdős problem 562
Let denote the -uniform hypergraph Ramsey number: the minimal such that if we -colour all edges of the complete -uniform hypergraph on vertices then there must be some monochromatic copy of the complete -uniform hypergraph on vertices.
Sources
FormalConjectures/ErdosProblems/
562.lean
Retained formal statement
Let denote the -uniform hypergraph Ramsey number: the minimal such that if we -colour all edges of the complete -uniform hypergraph on vertices then there must be some monochromatic copy of the complete -uniform hypergraph on vertices.
Prove that, for , where denotes the -fold iterated logarithm.
True ↔ ∀ r ≥ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑nOpenStatement only, no proof