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
For graphs, Spencer [Sp71] constructed a graph which contains cliques of at least different sizes, which Moon and Moser [MoMo65] showed to be best possible.
∃ C, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), ↑G.cliqueSizes.ncard ≤ ↑n - Real.logb 2 ↑n + CSolvedStatement only, no proof