The board / graph theory / #618
Erdős Problem #618
PROVED LEANdatabase updated 2026-02-08
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
For a graph `G` on `Fin n`, `h2 G` is the smallest number of edges that need to be added to `G` so that the resulting supergraph has diameter at most `2` (every two distinct vertices are adjacent or have a common neighbour) and is still triangle-free (`CliqueFree 3`). By the `sInf` convention on `ℕ`, `h2 G = 0` if no such supergraph exists.
For a triangle-free graph \(G\) let \(h_2(G)\) be the smallest number of edges that need to be added to \(G\) so that it has diameter \(2\) and is still triangle-free. Is it true that if \(G\) has maximum degree \(o(n^{1/2})\) then \(h(G)=o(n^2)\)? A problem of Erdős, Gyárfás, and Ruszinkó [EGR98]. Simonovits showed that there exist graphs \(G\) with maximum degree \(\gg n^{1/2}\) and \(h_2(G)\gg n^2\). Alon has observed this problem is essentially identical to [134], and his solution in [this note](https://web.math.princeton.edu/~nalon/PDFS/remark1901.pdf) also solves this problem in the affirmative.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/618.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/618
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.