---

Claim. For every $0<\eta<1$ and every sufficiently large $n$ there is a connected triangle-free graph $G$ on $n$ vertices with $h_4(G)\ge(1-\eta)n$, where $h_4$ counts the fewest edges whose addition gives a triangle-free supergraph of diameter at most four. No constant $c>0$ with $h_4(G)<(1-c)n$ for every connected triangle-free $G$ exists, so the question of Problem 619 has a negative answer. The construction attaches pendants to every vertex of a bounded-degree triangle-free core with small independence number; in any triangle-free diameter-four supergraph the pendant components untouched by new core edges are few, and almost every pendant is charged to a distinct added edge. The claimant is Nikolas Kuhn, who published the construction in a post of 14 June 2026 on the site's thread and owns the repository that holds the Lean proof. The site credits the counterexample to Claude Fable 5, prompted by Kuhn; Kuhn's post says that Claude Fable 5 found the disproof on 9 June 2026 and that Codex with GPT 5.5 formalized it under Fable's close guidance. Thomas Bloom's comment of 15 June 2026 optimizes the parameters to $h_4(G)\ge n-O(n^{8/9}(\log n)^{2/9})$ for infinitely many $n$. The corpus's rewritten proof, with the host-graph input and every counting lemma, is the result page main_theorem.

Acceptance. The site's curator, Thomas Bloom, accepted the disproof: the problem is labeled "SOLVED (LEAN)" (snapshot of 5 September 2026, page last edited 15 June 2026), the site's commentary credits the construction and records the strengthened bound, and the curator's own comments on the thread engage with the argument and derive that bound. The formal-conjectures statement erdos_619, in the statement file linked above as it stands at its last change of 18 September 2026, is tagged research solved with formal_proof links to the two artifacts above. That documented acceptance is the reviewed evidence. The repository's verification record reports a successful Lean 4.28.0 build, a kernel and comparator check, and the three standard axioms; the corpus has not built the proof or audited the formal statement against the question, so formalized is not listed. The rewritten proof on the library card is the project's own reading and warrants no evidence kind; no refereed write-up exists.