{"id":"palomar/PALOMAR-2026-10-17-000018","url":"https://github.com/jtraverso/moore-graphs-hoffman-singleton/tree/8819ccfea5474fab3d1cbc17e703860a4e008254","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000018-v1.json","repo":"https://github.com/jtraverso/moore-graphs-hoffman-singleton","tags":["math.CO","msc:05C50","msc:05C35","msc:05E30","moore-graphs","strongly-regular-graphs","lean","graph-theory"],"score":0,"title":"Moore graphs of diameter two: the Hoffman–Singleton theorem","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 Hoffman–Singleton theorem on Moore graphs of diameter two. For a finite k-regular graph of diameter at most two: the Moore bound n ≤ k² + 1; if moreover the girth is at least five, then n = k² + 1 and the graph is strongly regular with parameters (k² + 1, k, 0, 1); and, if k ≥ 2, then k ∈ {2, 3, 7, 57}. Mathlib has strongly regular graphs and the spectral theorem for Hermitian matrices, but not this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"On Moore Graphs with Diameters 2 and 3","identifier":"doi:10.1147/rd.45.0497","relationship":"formalizes"}]}