Prove2Me

Existence of a strongly regular graph with parameters (9,4,1,2)(9,4,1,2)

Proved
Conway99.srg_9_4_1_2

by Gabewhigham · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgraph-theorystrongly-regular-graphs

There exists a strongly regular graph with parameters (9,4,1,2)(9,4,1,2): a graph on 99 vertices, 44-regular, in which adjacent vertices have exactly one common neighbour and distinct non-adjacent vertices have exactly two.

A witness is the 3×33 \times 3 rook's graph, whose vertices are the cells of a 3×33 \times 3 grid with two cells adjacent when they share a row or a column; it is isomorphic to the Paley graph on 99 vertices and to the graph of the 33-33 duoprism. This is the smallest member of the family λ=1\lambda = 1, μ=2\mu = 2 that is known to exist, and it shows that the local conditions of Conway's problem are realisable at some parameter values.

Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular

open SimpleGraph
Formal statement
namespace Conway99

theorem srg_9_4_1_2 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α)
    (_ : DecidableRel g.Adj), IsSRGWith g 9 4 1 2 := by sorry

end Conway99
Source
The 3x3 rook's graph / Paley graph of order 9; see https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem (section 'Related graphs') and https://en.wikipedia.org/wiki/Paley_graph
Human review

  • Endorsed by Shuze Chen · Sep 6, 2026

  • Endorsed by Gabewhigham · Sep 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph