Machine-Checked Computational Group Theory in Lean 4: Operational Schreier-Sims Stabilizer Chains, BSGS Sifting, and Backtrack Ordered Partitions
Volkan Dağlı, Zerrin Dağlı, Dağhan Dağlı
cs.LO
Sep 29, 2026 · v1
cs.SC
TL;DR
Formalizes Schreier-Sims stabilizer chains, BSGS sifting, partition refinement, and residue/cyclotomic rings from GAP in Lean 4 with Mathlib4.
Abstract
We present gap-lean4-port (Release v0.2.0), a machine-checked formalization of foundational algorithms in computational discrete algebra and permutation group theory within the Lean 4 interactive theorem prover and Mathlib4. While modern proof assistants feature extensive abstract algebraic hierarchies, constructive and operational permutation group algorithms, such as Charles Sims' 1970 Schreier-Sims algorithm, transversal tree lookups, and backtrack ordered partition refinement, have remained largely unformalized in dependent type theory. Here, we formalize the operational algorithmic core of the Groups, Algorithms, Programming (GAP) system library across four foundational modules, proving 35 machine-checked theorems with zero unproven conjectures (sorry) and zero custom axioms under standard Lean 4 foundations (propext, Classical.choice, Quot.sound). We machine-check: (1) Schreier-Sims stabilizer chain hierarchies (StabLevel, StabChain) and the invariance of incremental transversal tree extensions (extendSchreierPoint_invariant); (2) single-level and multi-level Schreier sifting reductions (siftOneLevel, siftFull), proving that full sifting strictly fixes all base points (siftFull_fixes_all_basePoints); (3) constructive soundness and completeness of Base and Strong Generating Set (BSGS) membership testing (membershipTestKnownBase_iff_mem); (4) backtrack ordered partition cell refinement (splitCellByPred), proving mutual cell disjointness, union conservation, and exact cardinality preservation; (5) cyclotomic extension rings Z/nZ(eps_m) and machine-check GAP's exact size theorem |Z/nZ(eps_m)| = n^m; and (6) executable Bezout inverses via Extended Euclidean GCD (Nat.gcdA) over residue rings Z/nZ. The entire codebase compiles deterministically under 'lake build RequestProject' and is openly available at
https://github.com/pCwOrM/gap-lean4-port.
Problem
Operational permutation group algorithms, such as Schreier-Sims, transversal tree lookups, and backtrack ordered partition refinement, are largely unformalized in dependent type theory, even though proof assistants provide abstract algebraic hierarchies.
Approach
The authors port the algorithmic core of the GAP system library into Lean 4 and Mathlib4 across four modules. They define stabilizer chain structures (StabLevel, StabChain), single- and multi-level sifting (siftOneLevel, siftFull), BSGS membership testing, and partition cell splitting (splitCellByPred). They also formalize cyclotomic extension rings over Z/nZ and executable Bezout inverses via Nat.gcdA.
Results
35 theorems are machine-checked with no sorry and no custom axioms beyond propext, Classical.choice, and Quot.sound. The proved results include invariance of transversal extensions, full sifting fixing all base points, soundness and completeness of BSGS membership, partition disjointness and cardinality preservation, and |Z/nZ(eps_m)| = n^m.
