Counting identity for $\lambda = 1$ , $\mu = 2$ : $2n = k^2 + 2$

Proved

Conway99.srg_lambda_one_mu_two_card

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

combinatoricsgraph-theorystrongly-regular-graphs

Let $g$ be a strongly regular graph on a nonempty finite vertex set with parameters $(n,k,\lambda,\mu) = (n,k,1,2)$ : it has $n$ vertices, every vertex has exactly $k$ neighbours, adjacent vertices have exactly one common neighbour, and distinct non-adjacent vertices have exactly two common neighbours. Then

2n = k^2 + 2 .

This is the standard path-counting identity $k(k - \lambda - 1) = (n - k - 1)\mu$ for strongly regular graphs, specialised to $\lambda = 1$ and $\mu = 2$ . With $k = 14$ it forces $n = 99$ , which is where the parameter set of Conway's problem comes from. The hypothesis $0 < n$ excludes the empty vertex set, for which the conditions hold vacuously.

Preamble

import Mathlib.Combinatorics.SimpleGraph.StronglyRegular

open SimpleGraph

Formal statement

namespace Conway99

theorem srg_lambda_one_mu_two_card {V : Type*} [Fintype V] {g : SimpleGraph V}
    [DecidableRel g.Adj] {n k : ℕ} (h : g.IsSRGWith n k 1 2) (hn : 0 < n) :
    2 * n = k ^ 2 + 2 := by sorry

end Conway99

Source

Counting identity for strongly regular graphs, specialised to lambda = 1, mu = 2; cf. Mathlib SimpleGraph.IsSRGWith.param_eq and 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).
Endorsed by harry · Oct 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Counting identity for λ=1\lambda = 1λ=1, μ=2\mu = 2μ=2: 2n=k2+22n = k^2 + 22n=k2+2

Counting identity for $\lambda = 1$ , $\mu = 2$ : $2n = k^2 + 2$