Erdős problem 775 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

775.lean

Retained formal statement1 of 4

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

The answer is no, as proved by Gao [Ga25]: more generally, for any $k\geq 3$ , every $k$ -uniform hypergraph on $n$ vertices contains at most $n-f_k(n)$ different sizes of cliques, where $f_k(n)\to \infty$ as $n\to \infty$ .

FormalConjectures/ErdosProblems/775.leanErdos775.erdos_7751 lineExact file

1False ↔ ∃ C, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, n - C ≤ H.cliqueSizes.ncard

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science