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
Erdős, Gyárfás and Ruszinkó [EGR98]: every connected triangle-free graph on a finite vertex set can be extended, by adding edges, to a triangle-free graph of diameter at most . This shows that the infimum defining minNewEdges r G ranges over a nonempty set for every 3 ≤ r.
∀ {V : Type u_1} [Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ∃ H, G ≤ H ∧ H.CliqueFree 3 ∧ H.ediam ≤ 3SolvedStatement only, no proof