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]: for every connected triangle-free graph on vertices.
∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 5 G) ≤ (↑(Fintype.card V) - 1) / 2SolvedStatement only, no proof