kim@lean:~$ cat posts/2026·09·05.md
Certified graph isomorphism in Lean
I'm very excited to release HexGraphIso, a new sublibrary of Hex, which implements (a subset of) Brendan McKay's nauty in Lean, proves it correct, and provides a tactic layer.
nauty is one of my favourite pieces of software. It takes a decision problem, graph isomorphism, which is meant to be really hard, and uses a clever algorithm and heuristics to make it rather fast in practice! I didn't fully understand the beauty of nauty until I co-supervised one of Brendan's students, and could appreciate just how many combinatorial problems can be encoded into graph isomorphism problems, and then solved very efficiently with nauty.
The HexGraphIso library is a re-implementation of the dense graph algorithm from nauty, into Lean. Right now it only supports the default mode of operation, but I anticipate supporting further options from nauty later. We don't attempt to prove that the re-implementation is faithful (in practice, it is!), except via conformance tests. But we do prove that the Lean implementation is correct: two graphs are assigned the same "canonical form" if and only if they are isomorphic. Moreover we return efficient kernel checkable certificates for the canonical labelling.
In fact, most of the proof work goes into showing that the search pruning that nauty performs is all correct: that it never causes us to miss finding the canonical labelling.
This enables us to provide a graph_iso tactic, which solves both pairwise isomorphism and non-isomorphism goals, both without Mathlib (where graphs are represented using Hex.Graph, or Hex.GraphIso.Colored when you want ordered vertex colours) and with Mathlib, where the tactic gains the ability to process many ground terms representing SimpleGraphs.
Add to your lakefile.toml:
[[require]] name = "hex" git = "https://github.com/leanprover/hex.git" rev = "main"
and then:
import Hex
open Hex Hex.GraphIso
-- The Petersen graph as G(5,2), and as the Kneser graph K(5,2):
-- two presentations of the same graph on ten vertices.
def petersen : Graph 10 := Families.gpetersen 5 2
def kneser52 : Graph 10 := Families.kneser 5 2
example : Graph.Isomorphic petersen kneser52 := ⊢ petersen.Isomorphic kneser52 All goals completed! 🐙
-- The pentagonal prism G(5,1) also has ten vertices,
-- each of degree three.
def prism5 : Graph 10 := Families.gpetersen 5 1
example : ¬ Graph.Isomorphic petersen prism5 := ⊢ ¬petersen.Isomorphic prism5 All goals completed! 🐙
(This example is drawn from the Hex manual page for HexGraphIso.)
You might think that this is "only" about graphs. The real power of nauty and hence HexGraphIso
comes from the fact that a huge range of combinatorial objects can be encoded as graphs, moreover reflecting isomorphisms.
This then allows us to solve the isomorphism problem in many domains. In fact, the encoding doesn't need to be at all efficient,
because nauty is typically so efficient that the blowup doesn't matter much.
We illustrate this idea by taking the Latin square example from the nauty introduction
and implementing it using HexGraphIso.
Consider the Latin square whose rows are 0 2 1, 1 0 2, and 2 1 0.
The encoding has a vertex for each row, column,
symbol, and position, each kind receiving a different "color". Each position is
joined to its row, its column, and the symbol written there. A
colour-preserving graph isomorphism therefore restricts to three permutations,
and the three edges at every position force precisely the isotopy equation.
Once that correspondence is proved, the actual isotopy proof is just the
reduction followed by graph_iso:
open Hex.GraphIso.Mathlib
namespace LatinSquareExample
structure LatinSquare where
entry : Fin 3 → Fin 3 → Fin 3
rows : ∀ i, Function.Bijective (entry i)
columns : ∀ j, Function.Bijective (fun i => entry i j)
def Isotopic (L M : LatinSquare) : Prop :=
∃ r c s : Equiv.Perm (Fin 3),
∀ i j, M.entry (r i) (c j) = s (L.entry i j)
def nautySquare : LatinSquare where
entry
| 0, 0 => 0 | 0, 1 => 2 | 0, 2 => 1
| 1, 0 => 1 | 1, 1 => 0 | 1, 2 => 2
| 2, 0 => 2 | 2, 1 => 1 | 2, 2 => 0
rows := ⊢ ∀ (i : Fin 3),
Function.Bijective fun x =>
match i, x with
| 0, 0 => 0
| 0, 1 => 2
| 0, 2 => 1
| 1, 0 => 1
| 1, 1 => 0
| 1, 2 => 2
| 2, 0 => 2
| 2, 1 => 1
| 2, 2 => 0 All goals completed! 🐙
columns := ⊢ ∀ (j : Fin 3),
Function.Bijective fun i =>
match i, j with
| 0, 0 => 0
| 0, 1 => 2
| 0, 2 => 1
| 1, 0 => 1
| 1, 1 => 0
| 1, 2 => 2
| 2, 0 => 2
| 2, 1 => 1
| 2, 2 => 0 All goals completed! 🐙
def cyclicSquare : LatinSquare where
entry i j := ⟨(i + j) % 3, i:Fin 3j:Fin 3⊢ (↑i + ↑j) % 3 < 3 All goals completed! 🐙⟩
rows := ⊢ ∀ (i : Fin 3), Function.Bijective fun j => ⟨(↑i + ↑j) % 3, ⋯⟩ All goals completed! 🐙
columns := ⊢ ∀ (j : Fin 3), Function.Bijective fun i => ⟨(↑i + ↑j) % 3, ⋯⟩ All goals completed! 🐙
inductive Vertex
| row : Fin 3 → Vertex
| column : Fin 3 → Vertex
| symbol : Fin 3 → Vertex
| position : Fin 3 × Fin 3 → Vertex
deriving DecidableEq, Fintype
private def incidence (L : LatinSquare)
(x y : Vertex) : Prop :=
match x, y with
| .position (i, _), .row i' => i = i'
| .position (_, j), .column j' => j = j'
| .position (i, j), .symbol k => L.entry i j = k
| _, _ => False
private instance (L : LatinSquare) :
DecidableRel (incidence L) :=
fun x y => L:LatinSquarex:Vertexy:Vertex⊢ Decidable (incidence L x y)
L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝) y)L:LatinSquarey:Vertexa✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝) y) L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝) y)L:LatinSquarey:Vertexa✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝) y) L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.position a✝)) L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.position a✝))
L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable False L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (a✝¹.1 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (a✝¹.2 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (L.entry a✝¹.1 a✝¹.2 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable False All goals completed! 🐙
private def graph (L : LatinSquare) :
SimpleGraph Vertex :=
SimpleGraph.fromRel (incidence L)
private def color : Vertex → Fin 4
| .row _ => 0
| .column _ => 1
| .symbol _ => 2
| .position _ => 3
def encode (L : LatinSquare) :
Hex.GraphIso.Mathlib.Colored Vertex 4 where
graph := graph L
color := color
onto := L:LatinSquare⊢ Function.Surjective color All goals completed! 🐙
private instance (L : LatinSquare) :
DecidableRel (encode L).graph.Adj :=
fun x y => L:LatinSquarex:Vertexy:Vertex⊢ Decidable ((encode L).graph.Adj x y)
L:LatinSquarex:Vertexy:Vertex⊢ Decidable (x ≠ y ∧ (incidence L x y ∨ incidence L y x))
All goals completed! 🐙and then the correspondence itself, which is where the work is:
variable {L M : LatinSquare}
private def component : Fin 3 → Fin 3 → Vertex
| 0 => Vertex.row
| 1 => Vertex.column
| 2 => Vertex.symbol
private def index : Vertex → Fin 3
| .row i | .column i | .symbol i => i
| .position _ => 0
private def componentMap
(f : (encode L).Iso (encode M))
(kind i : Fin 3) : Fin 3 :=
index (f.graphIso (component kind i))
private theorem map_component
(f : (encode L).Iso (encode M))
(kind i : Fin 3) :
f.graphIso (component kind i) =
component kind (componentMap f kind i) := L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3⊢ f.graphIso (component kind i) = component kind (componentMap f kind i)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3hc:(encode M).color (f.graphIso (component kind i)) = (encode L).color (component kind i)⊢ f.graphIso (component kind i) = component kind (componentMap f kind i)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3v:Vertexh:f.graphIso (component kind i) = vhc:(encode M).color v = (encode L).color (component kind i)⊢ v = component kind (componentMap f kind i)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)
All goals completed! 🐙
private noncomputable def componentPerm
(f : (encode L).Iso (encode M)) (kind : Fin 3) :
Equiv.Perm (Fin 3) :=
Equiv.ofBijective (componentMap f kind) <| L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3⊢ Function.Bijective (componentMap f kind)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3⊢ Function.Injective (componentMap f kind)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3j:Fin 3h:componentMap f kind i = componentMap f kind j⊢ i = j
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3j:Fin 3h:componentMap f kind i = componentMap f kind jhc:component kind i = component kind j⊢ i = j
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨0, ⋯⟩) i = componentMap f ((fun i => i) ⟨0, ⋯⟩) jhc:component ((fun i => i) ⟨0, ⋯⟩) i = component ((fun i => i) ⟨0, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨1, ⋯⟩) i = componentMap f ((fun i => i) ⟨1, ⋯⟩) jhc:component ((fun i => i) ⟨1, ⋯⟩) i = component ((fun i => i) ⟨1, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨2, ⋯⟩) i = componentMap f ((fun i => i) ⟨2, ⋯⟩) jhc:component ((fun i => i) ⟨2, ⋯⟩) i = component ((fun i => i) ⟨2, ⋯⟩) j⊢ i = j L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨0, ⋯⟩) i = componentMap f ((fun i => i) ⟨0, ⋯⟩) jhc:component ((fun i => i) ⟨0, ⋯⟩) i = component ((fun i => i) ⟨0, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨1, ⋯⟩) i = componentMap f ((fun i => i) ⟨1, ⋯⟩) jhc:component ((fun i => i) ⟨1, ⋯⟩) i = component ((fun i => i) ⟨1, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨2, ⋯⟩) i = componentMap f ((fun i => i) ⟨2, ⋯⟩) jhc:component ((fun i => i) ⟨2, ⋯⟩) i = component ((fun i => i) ⟨2, ⋯⟩) j⊢ i = j All goals completed! 🐙
private theorem map_entry
(f : (encode L).Iso (encode M)) (i j : Fin 3) :
M.entry (componentMap f 0 i) (componentMap f 1 j) =
componentMap f 2 (L.entry i j) := L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position p⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (Vertex.position p) (component 1 (componentMap f 1 j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (Vertex.position p) (component 1 (componentMap f 1 j))hs:(encode M).graph.Adj (Vertex.position p) (component 2 (componentMap f 2 (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:p.1 = componentMap f 0 ihc:p.2 = componentMap f 1 jhs:M.entry p.1 p.2 = componentMap f 2 (L.entry i j)⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j)
All goals completed! 🐙
theorem isotopic_of_isomorphic :
(encode L).Isomorphic (encode M) → Isotopic L M := L:LatinSquareM:LatinSquare⊢ (encode L).Isomorphic (encode M) → Isotopic L M
L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)⊢ Isotopic L M
All goals completed! 🐙
example : Isotopic nautySquare cyclicSquare := L:LatinSquareM:LatinSquare⊢ Isotopic nautySquare cyclicSquare
L:LatinSquareM:LatinSquare⊢ (encode nautySquare).Isomorphic (encode cyclicSquare)
All goals completed! 🐙
end LatinSquareExampleFor now, we do not provide functions, verified or otherwise, that return generators for the automorphism group of a graph, but this will hopefully arrive soon.
Right now, HexGraphIso is about 5 to 12 times slower than nauty, and the non-isomorphism tactic, which replays the decision through the kernel, is about 5000 times slower again. (Already I'm very happy with these numbers: nauty is fast! We'll get a bit better with some further AI-driven optimization, but don't expect catching up!)
The first chart here shows canonical labelling over some standard families: a cactus plot of nauty 2.9.3 against the compiled canonicalize, and beside it the same two broken down per family against the number of vertices. Every family lands approximately an order of magnitude slower than nauty, with the Kneser and Johnson graphs the slowest and the grids and random graphs the quickest.
The second chart shows non-isomorphism proof obligations, which adds a third curve for the graph_iso tactic itself, timed end to end as a kernel-checked proof:
(Both measured on chungus2, an AMD EPYC 9455, on 2026-09-05. These charts also appear in the Hex manual page for HexGraphIso.)
Some other goodies associated with this release:
-
A specification of what the default dense mode of
nauty2.9.3 is actually doing! -
leanprover/nauty-ffi, a Lean FFI wrapper aroundnautyitself, if you don't care about verification and just want to run the original C code, fast. We don't use this inHexGraphIsoexcept for conformance testing.
Unreleased libraries, and all future development, live at github.com/kim-em/hex-dev. Contributions and pull requests are welcome, but specs must be updated before any new features or substantial changes, as separately reviewed PRs.