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

The complete bipartite graph Ka,bK_{a, b} has exactly a⋅ba \cdot b edges. The bound ⌊n2/4⌋\lfloor n^2 / 4 \rfloor in the Murty-Simon conjecture is attained by the balanced case K⌈n/2⌉,⌊n/2⌋K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}.

FormalConjectures/ErdosProblems/742.leanErdos742.complete_bipartite_edge_count1 lineExact file
∀ (a b : ℕ), (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b
TestStatement only, no proof