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

Open selected source

FormalConjectures/ErdosProblems/

742.lean

Retained formal statement5 of 5

Plesník [Pl75] proved the bound $|E(G)| < 3n(n-1)/8$ for any diameter- $2$ -critical graph on $n$ vertices.

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

1∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],2  Erdos742.IsDiameter2Critical G → ↑G.edgeFinset.card < 3 * ↑(Fintype.card V) * (↑(Fintype.card V) - 1) / 8

SolvedStatement only, no proof

Sources

Search problems.science