Pentagons in triangle-free graphs

DefinitionPentagons in triangle-free graphs (Erdős Problem 24)#✓fully proved

For every natural number \(n\), every graph on \(5n\) vertices with no three pairwise adjacent vertices has at most \(n^5\) subgraphs isomorphic to the \(5\)-cycle \(C_5\).

def conjecture : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 →
    G.copyCount (SimpleGraph.cycleGraph 5) ≤ n ^ 5

Used by 1

Used byPentagon bound for triangle-free graphs (five-cycle case of Erdős Problem 24)

TheoremPentagon bound for triangle-free graphs (five-cycle case of Erdős Problem 24)#●ready to prove

For every natural number \(n\), every graph on \(5n\) vertices with no three pairwise adjacent vertices has at most \(n^5\) subgraphs isomorphic to the \(5\)-cycle \(C_5\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Erdős Problems, Problem 24 (records the Grzesik and Hatami–Hladký–Králʼ–Norine–Razborov resolution), https://www.erdosproblems.com/24; Andrzej Grzesik, On the maximum number of five-cycles in a triangle-free graph, arXiv:1102.0962v3, https://arxiv.org/abs/1102.0962v3; Hamed Hatami, Jan Hladky, Daniel Kral, Serguei Norine, and Alexander Razborov, On the number of pentagons in triangle-free graphs, arXiv:1102.1634v4, https://arxiv.org/abs/1102.1634v4.

Uses 1

Statement usesPentagons in triangle-free graphs (Erdős Problem 24)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.