Skip to content

Erdős problem 742

Start work

Murty-Simon Conjecture

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

742.lean

Retained formal statement4 of 5

Füredi [Fü92] proved the Murty-Simon conjecture for all sufficiently large nn, that is, there exists n0n_0 such that every diameter-22-critical graph on n≥n0n \geq n_0 vertices has at most ⌊n2/4⌋\lfloor n^2 / 4 \rfloor edges.

FormalConjectures/ErdosProblems/742.leanErdos742.variants.furedi_bound3 linesExact file
∃ n₀,  ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],    n₀ ≤ Fintype.card V → Erdos742.IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4
SolvedStatement only, no proof