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

The complete bipartite graph $K_{a, b}$ has exactly $a \cdot b$ edges. The bound $\lfloor n^2 / 4 \rfloor$ in the Murty-Simon conjecture is attained by the balanced case $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$ .

FormalConjectures/ErdosProblems/742.leanErdos742.complete_bipartite_edge_count1 lineExact file

1∀ (a b : ℕ), (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b

TestStatement only, no proof

Sources

Search problems.science