---

Claim. The answer to Problem 24 is yes: every triangle-free graph on $5n$ vertices contains at most $n^5$ copies of $C_5$. The claimed result is Theorem 3 of Andrzej Grzesik, On the maximum number of five-cycles in a triangle-free graph: every triangle-free graph on $m$ vertices has at most $(m/5)^5$ unlabeled five-cycles. Substituting $m=5n$ gives the catalog's bound, which the balanced blow-up of $C_5$ (five independent sets of size $n$, consecutive parts joined completely) attains. The proof bounds the limiting induced-pentagon density by $24/625$ with flag algebras (Theorem 2) and converts the density bound into the finite count by a blow-up argument. Hatami, Hladký, Král', Norine and Razborov proved the same bound independently; their claim page also records the equality classification, which Grzesik's theorem alone does not give.

Acceptance. Refereed publication: J. Combin. Theory Ser. B 102 (2012), no. 5, 1061--1066, doi:10.1016/j.jctb.2012.04.001. The site's curator, Thomas Bloom, labels the problem proved and credits the answer to Grzesik [Gr12] and, independently, to Hatami, Hladký, Král', Norine and Razborov [HHKNR13]; the status search recorded on the problem page found no dispute of the result. The text cited is arXiv:1102.0962v3 (3 April 2012; v1 posted 4 February 2011, the date of this page); the journal text is not held. The flag-algebra coefficient calculations are not independently reviewed; the acceptance rests on the refereed publication and the curator's credit.

Formalization. A Lean 4 development declaring itself a formalization of Grzesik's proof was announced in the site's forum on 2026-04-23. Its header names Grzesik as the informal author and Matteo Del Vecchio and Aristotle as the formal authors, and describes the proof as Grzesik's two steps, the flag-algebra density bound $24/625$ and the conversion to the finite count. The copy hosted in Boris Alexeev's lean-proofs repository (Lean v4.29.1, 3,332 lines at the pinned commit of 2026-06-30, first added 2026-04-26) proves Erdos24.erdos_pentagon_conjecture: for every n : ℕ and every G : SimpleGraph (Fin (5 * n)) with G.CliqueFree 3, its count G.numC5 of five-cycles is at most n ^ 5. That count is the number of injective cyclic labelings divided by $10$; under triangle-freeness the file proves it equal to its own count numC5Copies of five-vertex sets carrying a five-cycle, as the problem page's Public formalization section records, and it never relates either count to Mathlib's copyCount, in which the formal-conjectures statement is written; it closes with #print axioms erdos_pentagon_conjecture and a comment reporting propext, Classical.choice and Quot.sound. The formal-conjectures statement of the problem names this copy in its formal_proof attribute, a second forum post of 2026-05-26 reports a version with native_decide removed, and the community database records formal_status Lean since 2026-04-23 (as of 2026-10-06). Nothing was built or replayed by this project, the axiom comment was not reproduced, and no independent whole-statement fidelity review is published, so the page lists no formalized evidence.