Documentation

FormalConjectures.ErdosProblems.«619»

Erdős Problem 619 #

References:

source
noncomputable def Erdos619.minNewEdges {V : Type u_1} (r : ℕ) (G : SimpleGraph V) :
ℕ

For a graph $G$, minNewEdges r G is the smallest number of edges that need to be added to $G$ so that it has diameter at most $r$, while preserving the property of being triangle-free. Erdős, Gyárfás and Ruszinkó denote this quantity by $h_r(G)$ in [EGR98].

Adding edges is formalised as passing to a supergraph H ≥ G on the same vertex set, the number of added edges being the (finite) cardinality of the edge set of H \ G. We use the extended diameter SimpleGraph.ediam (valued in ℕ∞) so that disconnected supergraphs, which have infinite diameter, do not qualify. If no triangle-free supergraph of G of diameter at most r exists, then minNewEdges r G = 0 by the Nat.sInf convention on the empty set; erdos_619.variants.add_edges_diam_three shows this degenerate case does not occur for connected triangle-free G when 3 ≤ r.

Equations
Instances For
    source
    theorem Erdos619.erdos_619 :
    False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)

    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$?

    The answer is no: for every $\eta>0$ there exist connected triangle-free graphs on $n$ vertices with $h_4(G)\geq(1-\eta)n$, so no such constant $c$ exists. The original proof was generated by Claude Fable 5; the Lean formalization was sketched by Fable and implemented by GPT 5.5 with Codex (see the linked formal_proof).

    source
    theorem Erdos619.erdos_619.variants.add_edges_diam_three {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    ∃ (H : SimpleGraph V), G ≤ H ∧ H.CliqueFree 3 ∧ H.ediam ≤ 3

    Erdős, Gyárfás and Ruszinkó [EGR98]: every connected triangle-free graph on a finite vertex set can be extended, by adding edges, to a triangle-free graph of diameter at most $3$. This shows that the infimum defining minNewEdges r G ranges over a nonempty set for every 3 ≤ r.

    source
    theorem Erdos619.erdos_619.variants.h_three_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    minNewEdges 3 G ≤ Fintype.card V

    Erdős, Gyárfás and Ruszinkó [EGR98]: $h_3(G) \leq n$ for every connected triangle-free graph $G$ on $n$ vertices.

    source
    theorem Erdos619.erdos_619.variants.h_five_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) (hG' : G.CliqueFree 3) :
    ↑(minNewEdges 5 G) ≤ (↑(Fintype.card V) - 1) / 2

    Erdős, Gyárfás and Ruszinkó [EGR98]: $h_5(G) \leq \frac{n-1}{2}$ for every connected triangle-free graph $G$ on $n$ vertices.

    source
    theorem Erdos619.erdos_619.variants.h_three_lower :
    ∃ c > 0, ∀ (n : ℕ), 0 < n → ∃ (V : Type) (x : Fintype V) (G : SimpleGraph V), Fintype.card V = n ∧ G.Connected ∧ G.CliqueFree 3 ∧ ↑n - c ≤ ↑(minNewEdges 3 G)

    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$.

    source
    theorem Erdos619.erdos_619.test.minNewEdges_eq_zero {V : Type u_1} {r : ℕ} {G : SimpleGraph V} (hG : G.CliqueFree 3) (hdiam : G.ediam ≤ ↑r) :
    minNewEdges r G = 0

    A triangle-free graph that already has diameter at most r needs no new edges.

    source
    theorem Erdos619.erdos_619.test.minNewEdges_singleton :
    minNewEdges 4 ⊥ = 0

    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.