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

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

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 ≪log⁡n/log⁡log⁡n\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,          ∀ n ≥ N,            ∀ (G : SimpleGraph (Fin n)),              G.CliqueFree 3 →                (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) →                  ∃ H,                    G ≤ H ∧                      H.CliqueFree 3 ∧                        (∀ (x y : Fin n), x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.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.