The Murty–Simon conjecture on diameter-2-critical graphs
A Lean 4 / Mathlib formalization of the proof by Sanjana Das and Jacob Fox of the Murty–Simon conjecture (arXiv:2610.39032, 2026). A graph is diameter-2-critical if its diameter is 2 and deleting any edge increases the diameter. Theorem 1.1: every diameter-2-critical graph on n vertices has at most ⌊n²/4⌋ edges (murty_simon), and a diameter-2-critical graph with ⌊n²/4⌋ edges is isomorphic to K_{⌈n/2⌉,⌊n/2⌋} (murty_simon_equality). Also: for n ≥ 3, K_{⌈n/2⌉,⌊n/2⌋} is diameter-2-critical with ⌊n²/4⌋ edges, so the bound is attained (murty_simon_sharp); Lemma 1.2, |E(G) \ M| ≤ |non-edges of G|…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000011/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'