Erdős problem 619

Erdős Problem 619 [EGR98, Er99]: For a triangle-free graph $G$ let $h_r(G)$ be the smallest number of edges that need to be added to $G$ so that it has diameter $r$ (while preserving the property of being triangle-free). Is it true that there exists a constant $c>0$ such that if $G$ is a connected graph on $n$ vertices then $h_4(G)<(1-c)n$?

The answer is no: for every $\eta>0$ there exist connected triangle-free graphs on $n$ vertices with $h_4(G)\geq(1-\eta)n$, so no such constant $c$ exists. The original proof was generated by Claude Fable 5; the Lean formalization was sketched by Fable and implemented by GPT 5.5 with Codex (see the linked formal_proof).