Skip to content

Erdős problem 775

Start work

Is there a 33-uniform hypergraph on nn vertices which contains at least n−O(1)n-O(1) different sizes of cliques (maximal complete subgraphs)?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

775.lean

Retained formal statement3 of 4

For graphs, Spencer [Sp71] constructed a graph which contains cliques of at least n−log⁡2n+O(1)n-\log_2n+O(1) different sizes, which Moon and Moser [MoMo65] showed to be best possible.

FormalConjectures/ErdosProblems/775.leanErdos775.erdos_775.variants.moon_moser1 lineExact file
∃ C, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), ↑G.cliqueSizes.ncard ≤ ↑n - Real.logb 2 ↑n + C
SolvedStatement only, no proof