Prove2Me

A 9999-graph has exactly 693693 edges

Proved
Conway99.conway_99_edgeFinset_card

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

combinatoricsgraph-theorystrongly-regular-graphs

Any strongly regular graph with parameters (99,14,1,2)(99,14,1,2) has exactly 693693 edges.

This is the handshake identity: the graph is 1414-regular on 9999 vertices, so the number of edges is 99⋅14/2=69399 \cdot 14 / 2 = 693. The statement is conditional on the existence of such a graph, which is Conway's open problem; it fixes one of the basic invariants any hypothetical 9999-graph must have.

Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular
import Mathlib.Combinatorics.SimpleGraph.Finite

open SimpleGraph
Formal statement
namespace Conway99

theorem conway_99_edgeFinset_card {V : Type*} [Fintype V] [DecidableEq V]
    {g : SimpleGraph V} [DecidableRel g.Adj] (h : g.IsSRGWith 99 14 1 2) :
    g.edgeFinset.card = 693 := by sorry

end Conway99
Source
Handshake identity for the parameters of Conway's 99-graph problem; https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem
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