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 statement3 of 5

Fan [Fa87] verified the Murty-Simon conjecture for all $n \leq 24$ and for $n = 26$ .

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

1∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],2  Fintype.card V ≤ 24 ∨ Fintype.card V = 26 →3    Erdos742.IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4

SolvedStatement only, no proof

Sources

Search problems.science