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
The graph with a single vertex is triangle-free and has diameter 0, so it needs no new edges to reach diameter at most 4.
Erdos619.minNewEdges 4 ⊥ = 0TestStatement only, no proof