{"id":"arxiv/2609.08319","url":"https://arxiv.org/abs/2609.08319","tags":["math.CO"],"score":0,"title":"Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof","domain":"math.CO","source":"arxiv","authors":["Kay Akiyama"],"reviews":0,"subject":"math.CO","summary":"We prove that no strongly regular graph with parameters $(266, 45, 0, 9)$ exists. The proof is formalized in Lean 4 and Mathlib without external infeasibility certificates or assumed classification theorems. A hypothetical graph gives a rank-$12$ integral Gram lattice with an integral centroid. A Lorentzian change of form, a marked $D_7$ gluing, and an explicit rank-six complement produce a positive-definite even unimodular lattice of rank $24$, together with the original indexed family of $220$ vectors. Harmonic theta identities and a root-isolation inequality force the root system $A_{11}…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-08","reactions":{}}