theorem Hex.GraphIso.Nauty.generators_complete {n k : Nat} {G : Colored n k} {p : Perm n} (hp : IsIso G G p) : Perm.Generated (List.filterMap (autom? G) (runColoredTraced G).autos.toList) p

Every automorphism is generated by the search's own checked output trace, including for the empty graph.