Status
On this page
Status
Topics
Status
On this page
Status
Topics
Let and be sufficiently large in terms of and . Let be a triangle-free graph on vertices with maximum degree .
Can be made into a triangle-free graph with diameter by adding at most edges?
Source: erdosproblems.com/134
An accepted solution exists. The statement is true.
PROVED (LEAN). Alon's published Theorem 3.2 gives a stronger quantitative bound and implies the exact fixed-, fixed- question as explained below; the site's curator credits Alon's note with the solution (claim page (Alon, 2024)). The site's label carries a Lean suffix for the Aristotle formalization of Alon's theorem reported on the thread, which is linked from the claim page and is not built or audited here. Search scope, 2026-10-07: the site's commentary and thread.