Erdős problem 619

Erdős Problem 619 [EGR98, Er99]: For a triangle-free graph $G$ let $h_r(G)$ be the smallest number of edges that need to be added to $G$ so that it has diameter $r$ (while preserving the property of being triangle-free). Is it true that there exists a constant $c>0$ such that if $G$ is a connected graph on $n$ vertices then $h_4(G)<(1-c)n$ ?

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

619.lean

Retained formal statement7 of 7

Erdős, Gyárfás and Ruszinkó [EGR98]: there is a constant $c > 0$ such that for every $n$ there exist connected triangle-free graphs $G$ on $n$ vertices with $h_3(G) \geq n - c$ .

FormalConjectures/ErdosProblems/619.leanErdos619.erdos_619.variants.h_three_lower2 linesExact file

1∃ c > 0,2  ∀ (n : ℕ), 0 < n → ∃ V x G, Fintype.card V = n ∧ G.Connected ∧ G.CliqueFree 3 ∧ ↑n - c ≤ ↑(Erdos619.minNewEdges 3 G)

SolvedStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures7
statement retained
VibeMathed1
statement retained
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean1
no statement retained
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki1
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 619.lean7