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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/134.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:134
  • PLBY Lean proofsErdosProblems.Erdos134

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page