发表机构
Anadolu University; ITouch Systems, Turkey; Mersin University, Turkey; Toros Science College, Turkey（阿纳多卢大学; ITouch系统公司; 梅尔辛大学; 托罗斯科学学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在 Lean 4 中形式化并机器验证了 GAP 系统库的核心置换群算法，包括 Schreier-Sims 稳定子链、BSGS 成员测试和回溯有序划分，证明了 35 个定理且无公理或未证明猜想。
AI 中文摘要
我们提出 gap-lean4-port（发布版 v0.2.0），这是在 Lean 4 交互式定理证明器及 Mathlib4 中对计算离散代数和置换群论中的基础算法进行的机器验证形式化。尽管现代证明助手具备广泛的抽象代数层级，构造性和操作式的置换群算法（如 Charles Sims 1970 年的 Schreier-Sims 算法、横截树查找和回溯有序划分细化）在依赖类型理论中仍 largely 未形式化。在此，我们形式化了 Groups, Algorithms, Programming (GAP) 系统库的操作式算法核心，涵盖四个基础模块，证明了 35 个机器验证定理，且零未证明猜想（sorry）和零自定义公理，基于标准 Lean 4 基础（propext、this http URL、this http URL）。我们机器验证了：(1) Schreier-Sims 稳定子链层级（StabLevel、StabChain）及增量横截树扩展的不变性（extendSchreierPoint_invariant）；(2) 单层和多层 Schreier 筛选归约（siftOneLevel、siftFull），证明完整筛选严格固定所有基点（siftFull_fixes_all_basePoints）；(3) 基和强生成集（BSGS）成员测试的构造性可靠性和完备性（membershipTestKnownBase_iff_mem）；(4) 回溯有序划分的单元细化（splitCellByPred），证明单元互不相交、并集守恒和基数精确保持；(5) 分圆扩张环 Z/nZ(eps_m) 及机器验证 GAP 的精确大小定理 |Z/nZ(eps_m)| = n^m；(6) 通过扩展欧几里得 GCD（this http URL）在剩余类环 Z/nZ 上实现可执行的 Bezout 逆元。整个代码库在 'lake build RequestProject' 下确定性编译，并公开于 this https URL。
英文摘要
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.
Comments3 pages, 1 table, Release v0.2.0, 35 machine-checked theorems with 0 sorry in Lean 4 / Mathlib4. Repository: https://github.com/pCwOrM/gap-lean4-port
