I wrote all of this in two days with Claude Code. The mathematical content is from my honours thesis (Symmetric Graphs and their Quotients, arXiv:1306.4798), extended with new results on the exceptional Chevalley group G₂(2) and its associated graphs.
The programme has two layers. The first is a library for algebraic graph theory in Mathlib.Combinatorics.SimpleGraph, developed across four PRs. PR #39530 introduces graph actions, vertex-transitivity, and arc-transitivity, connecting Mathlib's MulAction and SimpleGraph for the first time. PR #39548 defines the Sabidussi coset graph construction Sab(G, H, D), with the well-definedness proof that adjacency is independent of coset representatives. PR #39550 proves the Sabidussi representation theorem: every vertex-transitive graph is isomorphic to a coset graph. PR #39551 proves Lorimer's theorem characterising arc-transitive graphs via involutions, and the Lorimer quotient theorem showing that overgroups H ≤ K give graph quotients Sab(G, H, D) → Sab(G, K, KDK). A fifth library PR, #39653, develops CSS quantum codes from surface tilings: the chain complex condition ∂₁∘∂₂ = 0 and the main theorem k = 2g.
The second layer is twelve named graphs in Archive/, each exercising the abstract machinery in a different way. The dodecahedron quotients to the Petersen graph and the cube quotients to K₄, both by antipodal Z₂ involutions (#39650). The Heawood and Möbius-Kantor graphs are voltage graphs on K₂ with cyclic voltage groups Z₇ and Z₈ (#39651), and both also appear as genus-1 and genus-2 surface embeddings with CSS quantum codes encoding 2 and 4 logical qubits respectively (#39654). The Klein graph embeds on the Klein quartic (genus 3, 6 logical qubits) and is primitive — no interesting quotients exist (#39654).
The deepest results involve the exceptional group G₂(2) (order 12096) and the split Cayley hexagon GH(2,2). The Langer graph (63 vertices, 6-regular) is the collinearity graph of GH(2,2), and is proved isomorphic to the distance-2 graph of the Tutte 12-cage by composing two Sabidussi representation isomorphisms through a common coset graph (#39649). The Tutte 12-cage itself is semisymmetric: edge-transitive but not vertex-transitive, because GH(2,2) has no polarity over F₂. The dual Langer graph — the line-collinearity graph — shares the same intersection array but is proved non-isomorphic via a d₃-connectivity certificate (#39702). Both Langer and Zhou-6 are proved primitive by Atkinson's block-merging algorithm, and the Tutte 12-cage cannot cover the Langer graph because its point subgraph is edgeless (#39654).
The Zhou-3 graph (F182A, 182 vertices) is the first concrete instantiation of Lorimer's quotient theorem: its block system under D₁₂ gives the Zhou-6 graph, with arc-transitivity proved via an explicit involution of length 9 in the generators (#39695).
The Clayworth graph (4032 vertices, cubic) is the largest graph formally verified in Lean that I know of. It embeds on a genus-505 surface via the triangle group Δ(2,3,12), giving a CSS quantum code with 1010 logical qubits (#39654). The Meinhold family (#39698) consists of five quotient graphs of Clayworth, arising from intermediate subgroups between C₃ and G₂(2). These are new — they were discovered during this formalisation when a systematic enumeration of Clayworth's block systems showed that 83 of 85 intermediate subgroups give connected vertex-transitive quotients. The Langer graph is definitively not among them. The Meinhold family is named after Nick Meinhold, co-founder of Imagineering Melbourne.
I have left a handful of sorry's — dual graph regularity for the four surfaces and the Clayworth Sabidussi isomorphism where native_decide passes for each component but the kernel struggles to assemble the full 4032-vertex witness structure. I will fill these in over the next couple of weeks. The Clayworth graph definition is currently brute-force (flat adjacency array) and I plan to replace it with a cleaner algebraic definition derived from the triangle group.
The dependency order for reviewers is: #39530 → #39548 → #39550 → #39551, then #39653 independently. The Archive PRs depend on various combinations: #39649 depends on the Sabidussi/Lorimer chain, #39650 and #39651 depend on #39551, #39654 depends on #39653 and cross-references #39649 and #39651, #39695 depends on #39551 and #39654, #39698 depends on #39654, and #39702 depends on #39649.
I wrote all of this in two days with Claude Code. The mathematical content is from my honours thesis (Symmetric Graphs and their Quotients, arXiv:1306.4798), extended with new results on the exceptional Chevalley group G₂(2) and its associated graphs.
The programme has two layers. The first is a library for algebraic graph theory in Mathlib.Combinatorics.SimpleGraph, developed across four PRs. PR #39530 introduces graph actions, vertex-transitivity, and arc-transitivity, connecting Mathlib's MulAction and SimpleGraph for the first time. PR #39548 defines the Sabidussi coset graph construction Sab(G, H, D), with the well-definedness proof that adjacency is independent of coset representatives. PR #39550 proves the Sabidussi representation theorem: every vertex-transitive graph is isomorphic to a coset graph. PR #39551 proves Lorimer's theorem characterising arc-transitive graphs via involutions, and the Lorimer quotient theorem showing that overgroups H ≤ K give graph quotients Sab(G, H, D) → Sab(G, K, KDK). A fifth library PR, #39653, develops CSS quantum codes from surface tilings: the chain complex condition ∂₁∘∂₂ = 0 and the main theorem k = 2g.
The second layer is twelve named graphs in Archive/, each exercising the abstract machinery in a different way. The dodecahedron quotients to the Petersen graph and the cube quotients to K₄, both by antipodal Z₂ involutions (#39650). The Heawood and Möbius-Kantor graphs are voltage graphs on K₂ with cyclic voltage groups Z₇ and Z₈ (#39651), and both also appear as genus-1 and genus-2 surface embeddings with CSS quantum codes encoding 2 and 4 logical qubits respectively (#39654). The Klein graph embeds on the Klein quartic (genus 3, 6 logical qubits) and is primitive — no interesting quotients exist (#39654).
The deepest results involve the exceptional group G₂(2) (order 12096) and the split Cayley hexagon GH(2,2). The Langer graph (63 vertices, 6-regular) is the collinearity graph of GH(2,2), and is proved isomorphic to the distance-2 graph of the Tutte 12-cage by composing two Sabidussi representation isomorphisms through a common coset graph (#39649). The Tutte 12-cage itself is semisymmetric: edge-transitive but not vertex-transitive, because GH(2,2) has no polarity over F₂. The dual Langer graph — the line-collinearity graph — shares the same intersection array but is proved non-isomorphic via a d₃-connectivity certificate (#39702). Both Langer and Zhou-6 are proved primitive by Atkinson's block-merging algorithm, and the Tutte 12-cage cannot cover the Langer graph because its point subgraph is edgeless (#39654).
The Zhou-3 graph (F182A, 182 vertices) is the first concrete instantiation of Lorimer's quotient theorem: its block system under D₁₂ gives the Zhou-6 graph, with arc-transitivity proved via an explicit involution of length 9 in the generators (#39695).
The Clayworth graph (4032 vertices, cubic) is the largest graph formally verified in Lean that I know of. It embeds on a genus-505 surface via the triangle group Δ(2,3,12), giving a CSS quantum code with 1010 logical qubits (#39654). The Meinhold family (#39698) consists of five quotient graphs of Clayworth, arising from intermediate subgroups between C₃ and G₂(2). These are new — they were discovered during this formalisation when a systematic enumeration of Clayworth's block systems showed that 83 of 85 intermediate subgroups give connected vertex-transitive quotients. The Langer graph is definitively not among them. The Meinhold family is named after Nick Meinhold, co-founder of Imagineering Melbourne.
I have left a handful of sorry's — dual graph regularity for the four surfaces and the Clayworth Sabidussi isomorphism where native_decide passes for each component but the kernel struggles to assemble the full 4032-vertex witness structure. I will fill these in over the next couple of weeks. The Clayworth graph definition is currently brute-force (flat adjacency array) and I plan to replace it with a cleaner algebraic definition derived from the triangle group.
The dependency order for reviewers is: #39530 → #39548 → #39550 → #39551, then #39653 independently. The Archive PRs depend on various combinations: #39649 depends on the Sabidussi/Lorimer chain, #39650 and #39651 depend on #39551, #39654 depends on #39653 and cross-references #39649 and #39651, #39695 depends on #39551 and #39654, #39698 depends on #39654, and #39702 depends on #39649.