Erdős problem 24 · problems.science

Does every triangle-free graph on $5n$ vertices contain at most $n^5$ copies of $C_5$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

24.lean

Retained formal statement1 of 1

Does every triangle-free graph on $5n$ vertices contain at most $n^5$ copies of $C_5$ ?

Győri proved this with $1.03n^5$ , which has been improved by Füredi. The answer is yes, as proved independently by Grzesik [Gr12] and Hatami, Hladky, Král, Norine, and Razborov [HHKNR13].

FormalConjectures/ErdosProblems/24.leanErdos24.erdos_241 lineExact file

1True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 → G.copyCount (SimpleGraph.cycleGraph 5) ≤ n ^ 5

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