Problem 24

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

Graph theory

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

Proved. The site's label reads "PROVED (LEAN)"; the Lean proof it reports and its public scope are recorded below. The claim pages are Grzesik and Hatami, Hladký, Král', Norine and Razborov (both accepted on their refereed publications and the curator's credit); the 2026 Lean proof declares itself a formalization of Grzesik's proof and is recorded on that page as a formalization link; it gives no formalized evidence.

Er92b: Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240.
Er97f: Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. chapter at pp. 1-10.
Gr12: Grzesik, Andrzej, On the maximum number of five-cycles in a triangle-free graph. J. Combin. Theory Ser. B 102(5) (2012), 1061-1066. arXiv:1102.0962v3.
HHKNR13: Hatami, Hamed; Hladký, Jan; Král’, Daniel; Norine, Serguei; Razborov, Alexander, On the number of pentagons in triangle-free graphs. J. Combin. Theory Ser. A 120(3) (2013), 722-732. Published article; arXiv:1102.1634v4.

Problem 24

Status

Proof claims

Discussion