---

The claim. The $r$-blow-up of the cycle $C_{2k}$ (each vertex replaced by $r$ vertices and each edge by a complete bipartite graph between the two classes) has Turán number $O(n^{2-1/r+1/(k+r-1)+o(1)})$ (O. Janzer, Rainbow Turán number of even cycles, repeated patterns and blow-ups of cycles, Israel J. Math. 253 (2023), 813--840; arXiv:2006.01062, first posted 1 June 2020 as v1, which states the bound as its Theorem 1.14 and does not mention the Erdős--Simonovits conjecture; v2 of 20 July 2020 adds the conjecture and its disproof, so the disproof was first posted on 20 July 2020. The page keeps the v1 date because the result that disproves the problem, the blow-up bound, was first posted then, and the disproof is the elementary exponent comparison below). The blow-up is bipartite and $2r$-regular, so Problem 147 asks for the exponent $2-1/(2r-1)+\epsilon$; for $k$ large in terms of $r$ the proved exponent is smaller, so the problem's statement fails for every even minimum degree $2r\ge4$. The paper states the consequence as the disproof of an old conjecture of Erdős and Simonovits, and the site's commentary records it as the disproof for every even minimum degree at least 4.

What the corpus holds. The paper is carded on its source card (the card cites arXiv v3 of 12 April 2021), with the blow-up bound stated on the card and no result page; the exponent comparison in the paragraph above is elementary and is not a reading of the proof. The problem page's direct-proof compilation rests on the 3-regular counterexample of Janzer's later paper, which settles the problem on its own.

Acceptance. Refereed: Israel Journal of Mathematics, published online 17 November 2022. Reviewed: the site's curator, Thomas Bloom, credits this paper with the disproof for every even minimum degree at least 4 in the problem's commentary (erdosproblems.com/147, linked above, page last edited 18 January 2026, label DISPROVED (LEAN)). Formalization, not evidence: the site's page links the formal-conjectures statement erdos_147, whose formal_proof attribute names the file Erdos147.lean of Boris Alexeev's repository lean-proofs at the pinned commit (linked above). Its header names Janzer as informal author and the AI systems Codex and GPT-5.6 Sol as formal authors, and it proves not_erdos_147, the negation of the universal statement, by instantiating it at the single witness $C_{12}[2]$, the 2-blow-up of $C_{12}$, a $4$-regular bipartite graph whose extremal exponent the file bounds by $139/84<5/3$: the instance of minimum degree 4 ($r=2$, $k=6$) of this claim, and nothing about the other even degrees. At the pinned commit the main file (819 lines) and the four modules of the repository it imports in turn (Regularization, Conflict, Core and Basic, 2,838 lines together) contain no sorry, and Basic also imports the repository's module Erdos888.ColoredGraph. The corpus has not built or audited the file, so formalized is not listed.