Wilbrink (1984): a graph is not vertex-transitive
ProvedConway99.conway_99_not_vertex_transitivecombinatoricsgraph-theorystrongly-regular-graphs
No strongly regular graph with parameters is vertex-transitive: if is such a graph, then it is not the case that for every pair of vertices there is a graph automorphism of carrying to .
This is Wilbrink's theorem. In particular a hypothetical -graph cannot be a Cayley graph, which rules out the group-theoretic constructions that produce most known strongly regular graphs — including the two realised members of the family , , namely the Paley graph on vertices and the Berlekamp–van Lint–Seidel graph. The statement is a genuine restriction rather than a vacuous one only in the sense that existence is open; proving it does not require knowing whether such a graph exists.
Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular import Mathlib.Combinatorics.SimpleGraph.Maps open SimpleGraph
Formal statement
namespace Conway99
theorem conway_99_not_vertex_transitive {V : Type*} [Fintype V] {g : SimpleGraph V}
[DecidableRel g.Adj] (h : g.IsSRGWith 99 14 1 2) :
¬ ∀ v w : V, ∃ f : g ≃g g, f v = w := by sorry
end Conway99Source
H. A. Wilbrink, 'On the (99,14,1,2) strongly regular graph', in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342-355, https://research.tue.nl/files/2449333/256699.pdf ; as summarised in https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem
Human review
Confirmed by the mission captain (proposal self-audit).