---

Claim. Noga Alon's Theorem 3.2 in Problems and Results in Extremal Combinatorics--V (Bolyai Society Mathematical Studies 32, Springer, 2026, 13--29; article pp. 8--10): if a triangle-free graph $G$ on $n$ vertices has maximum degree at most $c(n)\sqrt n$, where $2(\log n)^{1/3}n^{-1/6}\le c(n)\le\frac1{10}$ and $n$ is large, then adding at most $2.5c(n)n^2$ edges gives a triangle-free graph of diameter at most two. For a sequence of triangle-free $n$-vertex graphs with maximum degree $d_n=o(\sqrt n)$, the choice $c(n)=\max\{d_n/\sqrt n,\,2(\log n)^{1/3}n^{-1/6}\}$ tends to zero and meets the hypotheses eventually, so $h_2(G_n)=o(n^2)$. This answers Problem 618 affirmatively as its corrected Statement asks it, with $h_2$ in the question, the function Erdős, Gyárfás and Ruszinkó call $h$, defined through diameter at most two; for $n\ge3$ the site's "diameter $2$" gives the same function, since a triangle-free completion cannot have diameter one. The theorem, its parameter transfer and its proof outline are on the result page theorem_3_2. The result first appeared in the author's 2024 note on Problem 134, where it is Theorem 1.2 (the two author versions carry the embedded dates 1 and 2 July 2024, the earliest dates known for the posting); the chapter gives the same theorem and proof as Theorem 3.2, and the same theorem is recorded on Problem 134's claim page.

Depends on. Nothing in this wiki; the argument is self-contained, and the problem page's account rests on this claim.

Formalization. The file src/v4.29.1/ErdosProblems/Erdos618.lean of Boris Alexeev's repository plby/lean-proofs, at the pinned commit linked above, declares itself a Lean formalization of a solution of Problem 618: its header names Alon as informal author and Aristotle and Alexeev as formal authors, and the file imports the repository's ErdosProblems.Erdos134, Alexeev's formalization of Alon's solution of Problem 134. Alexeev reported the file on the site's discussion thread on 8 February 2026, noting that it is the first solution on the site that imports another; the site's label carries a Lean suffix since. The formal-conjectures statement erdos_618, added by pull request 4371 (merged 3 August 2026) and linked above as a record at the merge commit, reads the question as: for every family $G_n$ of triangle-free graphs on $n$ vertices, if the maximum degree is $o(n^{1/2})$ then $h_2(G_n)=o(n^2)$, with $h_2$ defined through diameter at most two, the corrected Statement's question; it is tagged research solved and its formal_proof link points to the file above. The pull request records that its author cross-checked the statement against the hosted proof and that formal_proof links are given only where the hosted proof passed an axiom and hypothesis audit as unconditional. The corpus has not built Alexeev's proof file, and no statement-fidelity audit of it exists in this corpus, so formalized is not listed.

Acceptance. The site's curator, Thomas Bloom, labels the problem "PROVED (LEAN)" and credits Alon's note with the solution, recording Alon's observation that the problem is essentially the same as Problem 134; that credit is the reviewed evidence. The chapter is published by Springer in an edited volume; whether the volume's chapters were refereed is not established, so refereed is not listed. The project's own natural-language review of the reconstruction, dated 2026-09-05 on the source card, warrants no evidence kind.