Computational permutation groups in Lean
Hex now has a perm_group tactic, which uses the Schreier-Sims algorithm to answer many questions about permutation groups.
Here we calculate the order of the Mathieu group M11 (defined as a group generated by two permutations).
import HexPermGroupTheory
import Mathlib.GroupTheory.Perm.Cycle.Concrete
def M11 : Subgroup (Equiv.Perm (Fin 11)) :=
Subgroup.closure
{c[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10],
c[2, 6, 10, 7] * c[3, 9, 4, 5]}
example : Nat.card M11 = 7920 := ⊢ Nat.card ↥M11 = 7920
All goals completed! 🐙
example : c[0, 1] ∉ M11 := ⊢ (↑[0, 1]).formPerm ⋯ ∉ M11
All goals completed! 🐙
HexPermGroup contains the tactic, and
HexPermGroupTheory contains
additional glue that teaches the tactic how to work with Mathlib's permutations.
Starting from generators for a group of
permutations of {0, …, n - 1}, it computes a Schreier-Sims
stabilizer chain. Using this we can quickly do many things: compute the order, orbits and stabilizers,
test membership, write an element as a word in the generators, compare
subgroups, compute cosets, block systems and set transporters, and construct
derived series, direct products, and wreath products.
We can also ask for the enumeration index of an element in
(an arbitrary ordering of) the group, or ask for the i-th element,
without actually enumerating the group. These
operations take about n² steps per element, regardless of the order of the
group. We can efficiently generate random elements.
HexPermGroupTheory proves that these computations describe the subgroup of
Equiv.Perm (Fin n) generated by the same permutations. Its results include
the order theorem Group.order_card, the membership theorem contains_spec,
the block-system theorem blocks_spec, and sample_uniform.
The perm_group tactic packages the most immediately useful consequences. For
explicit permutations it proves goals of the forms
Nat.card (Subgroup.closure s) = N g ∈ Subgroup.closure s g ∉ Subgroup.closure s Subgroup.closure s = ⊤
and it can see through definitions such as M11 above.
How the tactic works
The tactic runs Schreier-Sims as compiled code, then copies the stabilizer chain into a compact certificate.
The Lean kernel then evaluates a Boolean checker on that certificate. When it succeeds, a soundness theorem, proved using Schreier's lemma and orbit-stabilizer, turns the result into a theorem about the generated subgroup.
For M11 the whole perm_group proof takes about 0.15 seconds.
The same mechanism reaches substantially larger examples. In an experiment
on a large workstation, total elaboration of a
perm_group proof for Co3, acting on 276 points and having order
495766656000, took 154 seconds and 3.8 GB.
The inputs were the ATLAS permutation generators.
That experiment also covered M11, M12, M22, M23, M24, J1, J2,
HS and McL, all within the default heartbeat limit.
Getting started
The
HexPermGroup manual chapter
covers the full computational interface, the Mathlib correspondence, the
certificate checker, graph automorphisms, and the bounded operations for
controlling time and output size.
To use the released Hex package, add this to your lakefile.toml:
[[require]] name = "hex" git = "https://github.com/leanprover/hex.git" rev = "main"
For Mathlib-free computation, use
import HexPermGroup
For the correspondence theorems and perm_group, use
import HexPermGroupTheory
The example above additionally imports
Mathlib.GroupTheory.Perm.Cycle.Concrete for the c[...] cycle notation.
There is an approved Tau Ceti roadmap proposal to prove the orders of these ten sporadic groups and connect them to the presentations used in Tau Ceti.
Unreleased libraries and future development live at github.com/kim-em/hex-dev. Discussion is welcome at #Computer algebra > Discussion: Hex on the Lean Zulip.