Erdős problem 619
Erdős Problem 619 [EGR98, Er99]: For a triangle-free graph let be the smallest number of edges that need to be added to so that it has diameter (while preserving the property of being triangle-free). Is it true that there exists a constant such that if is a connected graph on vertices then ?
Sources
FormalConjectures/ErdosProblems/
619.lean
Retained formal statement
A triangle-free graph that already has diameter at most r needs no new edges.
∀ {V : Type u_1} {r : ℕ} {G : SimpleGraph V}, G.CliqueFree 3 → G.ediam ≤ ↑r → Erdos619.minNewEdges r G = 0TestStatement only, no proof