Erdős problem 742 · problems.science

Murty-Simon Conjecture

Sources

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

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

742.lean

Retained formal statement4 of 5

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

FormalConjectures/ErdosProblems/742.leanErdos742.variants.furedi_bound3 linesExact file

1∃ n₀,2  ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],3    n₀ ≤ Fintype.card V → Erdos742.IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4

SolvedStatement only, no proof

Sources

Search problems.science