Conway's 99-graph problem: a strongly regular graph with parameters
OpenConway99.conway_99Conway's 99-graph problem. Does there exist an undirected graph on vertices in which every two adjacent vertices have exactly one common neighbour and every two distinct non-adjacent vertices have exactly two common neighbours? Equivalently: every edge lies in a unique triangle, and every non-adjacent pair is the pair of opposite corners of a unique quadrilateral. Such a graph is necessarily -regular, i.e. strongly regular with parameters .
The statement asserts the existence of a finite type carrying a simple graph with , and is Mathlib's proof_wanted conway_99 verbatim. The problem is open: no such graph is known, and no non-existence proof is known. John Horton Conway offered $1000 for a solution. A disproof — a proof that no such graph exists — resolves the problem just as well as a construction.
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular open SimpleGraph
namespace Conway99
theorem conway_99 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α)
(_ : DecidableRel g.Adj), IsSRGWith g 99 14 1 2 := by sorry
end Conway99
Confirmed by the mission captain (proposal self-audit).