Skip to content

Erdős problem 742

Murty-Simon Conjecture

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

742.lean

Retained formal statement2 of 5

Murty-Simon Conjecture

Let GG be a graph on nn vertices with diameter 22 such that deleting any edge increases the diameter. Is it true that GG has at most ⌊n2/4⌋\lfloor n^2 / 4 \rfloor edges? Equality is conjectured to hold for the complete balanced bipartite graph K⌈n/2⌉,⌊n/2⌋K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}.

The conjecture is resolved up to a finite check: Fan [Fa87] verified it for n≤24n \leq 24 and n=26n = 26, and Füredi [Fü92] proved it for all sufficiently large nn.

FormalConjectures/ErdosProblems/742.leanErdos742.erdos_7423 linesExact file
True ↔  ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],    Erdos742.IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4
OpenStatement only, no proof