---

Noga Alon, Problems and Results in Extremal Combinatorics--V, in Sum(m)it280, Bolyai Society Mathematical Studies 32, Springer (2026), 13--29, DOI 10.1007/978-3-032-18810-6_2, first published online 2026-05-28; Problem 3.1 and Theorem 3.2, article pp. 8--10. The result first appeared in the author's note Triangle-free graphs of diameter 2 (Problem 1.1 and Theorem 1.2), posted on the author's publication list and linked by the site; two versions of the note are posted, whose embedded dates are 1 and 2 July 2024, and the second adds a remark on what the author learned after posting the note, so the page name carries the first version's embedded date as the first posting. The chapter is filed (card; [[../library/extremal_graph_theory/alon_2026_problems_results_extremal_combinatorics_v/theorem_3_2|theorem page]]).

The result. Theorem 3.2: let $G$ be a triangle-free graph on $n$ vertices with maximum degree at most $c(n)\sqrt n$, where

$$2\frac{(\log n)^{1/3}}{n^{1/6}}\le c(n)\le\frac1{10}$$

and $n$ is large. Then at most $2.5c(n)n^2$ edges can be added to $G$ to obtain a triangle-free graph of diameter two. The proof runs a bounded-degree triangle-free process whose outcome has independence number below $5c(n)n$ with high probability, completes it to a maximal triangle-free graph, and bounds the degrees by the independence number. For the problem's fixed $\epsilon,\delta>0$, choose $0<\epsilon_0<\min\{\epsilon,1/6\}$ and $c(n)=n^{-\epsilon_0}$: the degree hypothesis $\Delta(G)<n^{1/2-\epsilon}$ implies $\Delta(G)\le c(n)\sqrt n$, the theorem's range holds for large $n$, and fewer than $2.5n^{2-\epsilon_0}<\delta n^2$ edges are added. So the answer to the question is yes, and the theorem page records the deduction step by step. The same theorem resolves Problem 618, the $o(\sqrt n)$ form of the question.

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/latest/ErdosProblems/Erdos134.lean of Boris Alexeev's repository plby/lean-proofs (import Mathlib its only import; pinned at a commit of 2026-08-22, the Lean file itself last changed on 2026-08-12) declares itself a formalization of this result: its header names Alon as informal author and Aristotle and Alexeev as formal authors. A comment of 8 February 2026 on the site's thread by Alexeev reported the file with an online type-check route, and the site's label carries a Lean suffix since. In namespace Erdos134 the file proves theorem_1_2, the theorem above for a $K_3$-free graph on $n\ge1000$ vertices with every degree at most $c\sqrt n$, under the paper's range for $c$ together with $c\sqrt n\ge4$ and an explicit binomial bound $\binom n{\lfloor5cn\rfloor}\le2^{10cn\log(1/c)}$, and erdos_134, the problem's statement with diameter $2$ read as every two distinct vertices adjacent or at distance two: for all real $\epsilon,\delta>0$ there is $N$ such that every $K_3$-free graph on $\mathrm{Fin}\,n$, $n\ge N$, with every degree below $n^{1/2-\epsilon}$ has a $K_3$-free supergraph of that kind with at most $\delta n^2$ added edges. At the pin the file has no sorry and closes with a #print axioms erdos_134 comment reporting propext, Classical.choice and Quot.sound, the file's own report. The file is not built, kernel-checked or audited by this corpus, and no outside examination of it is published, so the page lists no formalized evidence.

Acceptance. The site's curator, Thomas Bloom, marks the problem "PROVED (LEAN)" and credits Alon's note in the commentary, which states that it solves the problem in a strong form; that credit is the reviewed evidence, and Bloom took no part in the note or the chapter. The chapter is published in a Springer book series; whether the volume's chapters were refereed is not documented, so refereed is not listed. The complete rewritten proof and the exact deduction were reviewed on 2026-09-05 in the [[../library/extremal_graph_theory/alon_2026_problems_results_extremal_combinatorics_v/evidence/verify/theorem_3_2_review|Theorem 3.2 review]] filed with the source; that is this project's own proof coverage, not acceptance evidence, and it is not listed under evidence.