Checking the machinery behind permutation-group calculations
- What it is
- A short paper reports machine-checked versions of several working algorithms in computational group theory.
- Who did it
- Volkan Dağlı, Zerrin Dağlı, and Dağhan Dağlı.
- What it could mean
- If the code and stated assumptions check out, parts of computer algebra could become easier to inspect as executable mathematics.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Machine-Checked Computational Group Theory in Lean 4: Operational Schreier-Sims Stabilizer Chains, BSGS Sifting, and Backtrack Ordered Partitions ↗See the proposed checks
Pin repository release and Lean/mathlib versions; inspect named theorem statements and axioms; compare encoded assumptions to GAP semantics, with a separately authorized isolated build if needed.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
Symmetry operations with one position fixed
Keeping one position fixed while rearranging others introduces a stabilizer. The paper formalizes selected permutation-group algorithms in Lean. These objects illustrate the idea, not an execution trace or verified output.
Read the source · Sections 3–5 · stabilizer chains, membership, and partition refinement ↗- What it claims
- The three-page paper reports 35 machine-checked theorems across four modules, selected stabilizer-chain and partition algorithms, and residue-ring results. This overdue intake does not claim verification of every GAP algorithm or its implementation.
- Why this could matter
- Checking the machinery behind permutation-group calculations Computer algebra depends on routines that sift permutations through stabilizer chains. This work reports Lean proofs for selected routines and their invariants, making their mathematical behavior inspectable rather than relying only on tests.
- If it holds up
- It would provide a reusable formal base for selected permutation-group and partition-search computations.
- If it does not
- A mismatch in assumptions, definitions, or the release build would reveal which claimed algorithmic guarantee is narrower than advertised.
- Impact horizon
- Methods · Computational group theory · Computer algebra · Formalization
- Version
- submitted 2026-09-29 20:21:25 UTC
- Why we tracked it
- unexamined mathematical formalization intake, not a proof verdict or homepage feature.
- Highest-risk dependency
- BSGS completeness assumes complete transversals; the ring cardinality result is representation-specific. Zero-sorry and deterministic-build claims remain author reports.
- Available artifacts
- gap-lean4-port release v0.2.0 at https://github.com/pCwOrM/gap-lean4-port and related Zenodo DOI 10.5281/zenodo.23045504. No build, axiom examination, or correspondence check was run.
- Current boundary
- Intake record only; examination not started.