The board / graph theory / #742
Erdős Problem #742
DECIDABLEdatabase updated 2025-08-31
Still open, but reduced to a finite computation: checking enough cases would settle it either way.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A graph is diameter-2-critical if it has diameter \(2\) and removing any edge increases the diameter beyond \(2\).
**Murty-Simon Conjecture** Let \(G\) be a graph on \(n\) vertices with diameter \(2\) such that deleting any edge increases the diameter. Is it true that \(G\) has at most \(\lfloor n^2 / 4 \rfloor\) edges? Equality is conjectured to hold for the complete balanced bipartite graph \(K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}\). The conjecture is resolved up to a finite check: Fan [Fa87] verified it for \(n \leq 24\) and \(n = 26\), and Füredi [Fü92] proved it for all sufficiently large \(n\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/742.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/742
Attempts
submit one →Read our working report →
Exact reproducible checks find no counterexample through n=14 and reduce the first open order n=25 to five SAT instances (maximum degree 13 through 17); the uniform conjecture remains open.
PARTIAL