{"id":"palomar/PALOMAR-2026-11-01-000011","url":"https://github.com/jtraverso/murty-simon-conjecture/tree/adadd2fbd0ba9e9c71faadd105f357f7b12a814f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000011-v1.json","repo":"https://github.com/jtraverso/murty-simon-conjecture","tags":["math.CO","msc:05C35","msc:05C12"],"score":0,"title":"The Murty–Simon conjecture on diameter-2-critical graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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|…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"A proof of the Murty–Simon conjecture on diameter-2-critical graphs","identifier":"arXiv:2610.39032","relationship":"formalizes"}]}