---

Claim. Kenta Kitamura announces, in thread comments of 7 and 8 September 2026 and the repository KitaKen1/erdos-612-lean, Lean 4 files for the fixed-clique cases of [[problems/extremal_graph_theory/E0612/_index|Problem 612]] left open by the counterexamples to part (i). The thread comment and the repository's first commit of 7 September, like Kitamura's issue-828 comment of that day, carry only the proved cases ($r=2$, $k=3,4$) and list the $K_7$ case as open; the $r=3$ refutation, on which this claim's value rests, was added to the repository and announced in the thread on 8 September 2026. Part (ii) at $r=3$ ($K_7$-free graphs, bound $\frac83\frac n\delta+O(1)$ for $8\mid\delta$) is refuted: the repository's README describes a $71$-layer periodic $K_7$-free family of minimum degree $800$, order $n=21296p+960$ and diameter at least $71p+1$ for every positive integer $p$; the conjectured main term at $\delta=800$ is $\frac83\cdot\frac{21296p+960}{800}=\frac{5324}{75}p+\frac{16}5$, so the diameter exceeds it by at least $\frac p{75}-\frac{11}5$, unbounded in $p$, and no additive constant restores the inequality (the theorem erdos_612.variants.original_k7, stated as answer(False)). Since $8\mid800$, the same family refutes the amended conjecture of Czabarka, Singgih and Székely at $k=6$ (amended_k6). The files also prove part (ii) at $r=2$ in the form $2d(D+1)+4\le5n$ for every connected $K_5$-free finite graph, without the divisibility hypothesis $5\mid d$ (original_k5), prove the amended conjecture for $k=3$ (as $3d(D+1)+6\le7n$ for connected $K_4$-free graphs) and $k=4$, and refute it for $k=5$; the proved cases use a strong reading of the $O(1)$ term, with constant $0$, which implies the stated $O(1)$ form. The comments report that the files contain no sorry, that #print axioms lists only propext, Classical.choice and Quot.sound, and that the formalization and proofs were prepared, in the words of the README's AI disclosure, with assistance from OpenAI Codex, Astra, and ChatGPT under Kitamura's direction; the amended conjecture is not the problem.

Covers. Part (ii). The $r=3$ refutation is one false instance of part (ii), which is asked for every $r$ and every admissible $\delta$, so if accepted it disproves part (ii) in full, as would the page of [[problems/extremal_graph_theory/E0612/claims/2026_09_03_chen_chen|Chen and Chen]]; since part (i) is already disproved, the problem would then be disproved. The proof at $r=2$ is a partial result on part (ii) and settles nothing by itself. It does not bear on part (i).

Standing. Claimed. The corpus has not built these Lean files, so they give no formalized evidence, and no statement-fidelity audit of them exists in this corpus; the site marks comments as unverified. A comment of 8 September 2026 by one of the authors of the 2025 counterexample says the same conclusions for $r=2$ (true) and $r=3$ (false) were reached independently, without a posted argument. Kitamura's comment of 7 September 2026 on formal-conjectures issue 828 (opened by another user in October 2025) links a draft statement and its strong and weak formalizations of the $O(1)$ term; no file ErdosProblems/612.lean was found there. If the announcements hold, part (ii) is true exactly for $r\in\{1,2\}$, and so disproved. Part (ii) stays open until a refutation of it is accepted.