Skip to content

Erdős problem 134

Let ϵ,δ>0\epsilon,\delta>0 and nn be sufficiently large in terms of ϵ\epsilon and δ\delta. Let GG be a triangle-free graph on nn vertices with maximum degree <n1/2ϵ<n^{1/2-\epsilon}. Can GG be made into a triangle-free graph with diameter 22 by adding at most δn2\delta n^2 edges?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

134.lean

Retained formal statement1 of 1

Let ϵ,δ>0\epsilon,\delta>0 and nn be sufficiently large in terms of ϵ\epsilon and δ\delta. Let GG be a triangle-free graph on nn vertices with maximum degree <n1/2ϵ<n^{1/2-\epsilon}. Can GG be made into a triangle-free graph with diameter 22 by adding at most δn2\delta n^2 edges?

Asked by Erdős and Gyárfás, who proved that this is the case when GG has maximum degree logn/loglogn\ll \log n/\log\log n. A construction of Simonovits shows that this conjecture is false if we just have maximum degree Cn1/2\leq Cn^{1/2}, for some large enough CC. In this note Alon solves this problem in a strong form, in particular proving that a triangle-free graph on nn vertices with maximum degree <n1/2ϵ<n^{1/2-\epsilon} can be made into a triangle-free graph with diameter 22 by adding at most O(n2ϵ)O(n^{2-\epsilon}) edges.

FormalConjectures/ErdosProblems/134.leanErdos134.erdos_13414 linesExact file
True  ∀ (ε δ : ℝ),    0 < ε →      0 < δ →N,nN,            ∀ (G : SimpleGraph (Fin n)),              G.CliqueFree 3 →                (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) →H,                    GH                      H.CliqueFree 3 ∧                        (∀ (x y : Fin n), xyH.Adj x y ∨ ∃ z, H.Adj x zH.Adj z y) ∧                          ↑(H.edgeFinset \ G.edgeFinset).card ≤ δ * ↑n ^ 2
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page