Erdős problem 775
Is there a -uniform hypergraph on vertices which contains at least different sizes of cliques (maximal complete subgraphs)?
Sources
FormalConjectures/ErdosProblems/
775.lean
Retained formal statement
The answer is no, as proved by Gao [Ga25]: more generally, for any , every -uniform hypergraph on vertices contains at most different sizes of cliques, where as .
∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : ThreeUniformHypergraph (Fin n)), H.cliqueSizes.ncard + f n ≤ nSolvedStatement only, no proof