Research Transition Tutorial · 2026

从群论到机器证明

以 Isabelle/HOL 为主工具，从有限群作用进入对称性约化、计算证书与可信数学证明。

方向决定。 主工具选择 Isabelle/HOL；数学主线选择有限群作用与对称性；方法主线选择可核验计算、证明诊断与证明修复。

十二周目标。 完成一个“有限着色的对称性约化证书”原型：外部程序寻找轨道代表元，Isabelle 独立证明证书的正确性与覆盖性。

方向 工具 数学阶梯 Starter Lab 十二周 研究实验 资料

1. 研究定位：不是“用 AI 做数学”

数学对象

群、子群、同态、商群、群作用、轨道、稳定子、Sylow 理论、有限表示，以及它们在对称结构中的作用。

计算对象

有限着色、轨道代表元、图自同构、枚举与剪枝、SAT/SMT 结果，以及可以独立检查的计算证书。

可信对象

不把 Python、GAP、LLM 或搜索器直接当作证明；让它们生成候选结果和证书，再由 Isabelle 的逻辑内核核验。

研究对象

证明如何失效、诊断信息如何帮助修复、数学库演化如何影响证明，以及自动化怎样在不扩大可信基的前提下工作。

你的新研究身份：研究群论结构如何压缩计算搜索空间，并研究计算结果如何转化为机器可检查的数学证据。

2. 数学北极星：对称性约化的可信证明

设有限群 G 作用在有限对象集合 X 上。对象可能是字符串、图着色、组合构型或协议状态。我们不逐个检查 X 中的全部对象，而是按轨道划分，只计算代表元。

数学层：证明作用、轨道、稳定子与商空间的性质。
计算层：生成轨道代表元、固定点计数或剪枝结果。
证书层：记录“为什么没有遗漏，也没有重复”。
Isabelle 层：证明检查器接受证书，就意味着原命题成立。

这条线可以从循环群作用下的项链计数开始，发展到二面体群作用下的多边形着色，再进入图自同构作用下的图着色。长期目标不是重做四定理，而是建设可用于“四定理式大规模组合证明”的对称性约化与证书基础设施。

3. 为什么先学 Isabelle/HOL

实验室知识链

李勇坚老师长期研究基于 Isabelle 的定理证明与参数化验证；吕毅老师长期从事形式化验证和模型检测。近距离讨论问题、代码和证明，比单独追逐最热工具更有研究价值。

李勇坚老师主页 · 吕毅老师主页

群论基础已存在

Isabelle/HOL 与 AFP 已有群作用、轨道—稳定子、Sylow 定理、有限生成阿贝尔群和有限群表示论等正式发展，可以从成熟库进入真正的数学。

自动化但不失控制

simp、auto、Sledgehammer、Nitpick 和代码生成覆盖证明、反例搜索和可执行检查；最终证明项仍由 Isabelle 检查。

Lean 放到第二阶段

Lean 与 Mathlib 仍值得学习，尤其适合观察 AI 定理证明生态。但第一阶段同时学习两套系统会稀释数学进度。先在 Isabelle 做出一个完整 artifact，再做跨证明器比较。

Installation

固定版本与工作环境

  1. 安装当前正式版 Isabelle2025-2，使用自带的 Isabelle/jEdit。
  2. 第一周只使用发行版自带文档和 HOL；不要立刻安装大量插件。
  3. 第二周再安装与正式版匹配的 Archive of Formal Proofs。
  4. 所有实验建立独立 session，固定 Isabelle 与 AFP 版本，并让命令行构建可重复。
isabelle version
isabelle components -u /path/to/afp/thys
isabelle build -D .

4. 群论的数学阶梯

Level 1群、公理与同态群的两种表示方式；子群、正规子群、核与像；第一同构定理；Lagrange 定理。目标是学会把纸面定义翻译成 HOL 类型、集合、locale 和 type class。
Level 2群作用轨道、稳定子、固定点、共轭作用与轨道—稳定子定理。目标是能够阅读并重建 AFP 的群作用证明，而不是只调用现成结论。
Level 3有限群结构Sylow 定理、循环群、有限阿贝尔群分解。目标是理解形式化中哪些“显然”步骤最昂贵，以及库抽象如何影响证明。
Level 4表示与对称性群环、模、Maschke 定理、Schur 引理和有限群表示。先阅读已有形式化，再选择一个小而真实的缺口，不重复搬运教材。
Level 5组合结构上的作用循环群与二面体群作用于项链、多边形着色和图着色；研究 Burnside 型计数、轨道代表元和自同构约化。
Level 6计算证书让 Python 或 GAP 做大计算，让 Isabelle 验证证书的 soundness、completeness 和无重复性。这里开始形成独立研究贡献。

5. Starter Lab：第一天必须跑通

先用 Isabelle/HOL 的 type-class 群完成一个最小理论文件。这个练习不是数学贡献，而是检查环境、符号、自动化和命令行构建是否全部贯通。

Group_Warmup.thy

逆元与共轭

theory Group_Warmup
  imports Main
begin

lemma inverse_of_product:
  fixes a b :: "'a::group"
  shows "inverse (a * b) = inverse b * inverse a"
  by simp

lemma conjugation_preserves_product:
  fixes g a b :: "'a::group"
  shows "g * (a * b) * inverse g =
         (g * a * inverse g) * (g * b * inverse g)"
  by (simp add: mult.assoc)

end

完成后做三件事：让 Sledgehammer 给出另一种证明；删掉一个结合律提示观察失败信息；把第二条改写成结构化 Isar 证明，明确每一步取消逆元的位置。

First mathematical lab

循环群作用下的二进制项链

  1. 定义长度 n 的二进制串以及循环移位。
  2. 证明所有移位组成循环群在串集合上的作用。
  3. 定义轨道等价和 canonical representative。
  4. 写一个可执行函数枚举代表元。
  5. 证明枚举结果无重复并覆盖所有轨道。
  6. 对 n = 4, 5, 6 计算结果，与独立 Python 枚举交叉核对。

升级：加入反射得到二面体群；再把串替换为多边形顶点着色。这一步自然进入群作用、固定点与 Burnside 型计数。

6. 十二周学习与研究计划

Week 1HOL 与构建完成 Programming and Proving 的函数、归纳、集合和 Isar 部分；建立可命令行构建的 session。交付 8—10 个小 theory。
Week 2证明工具系统练习 simp、auto、blast、Sledgehammer、Nitpick、find_theorems。每个自动证明都能解释依赖了什么。
Week 3–4基础群论重建子群、同态、核、像、Lagrange 和第一同构定理中的代表性引理；比较 type class 与 HOL-Algebra locale。
Week 5–6群作用阅读 Orbit-Stabiliser 和 Secondary Sylow；独立实现循环群作用下的项链与二面体着色。
Week 7–8图与证书阅读 Planarity Certificates 的架构；定义有限图着色、图自同构作用和代表元证书的规格。
Week 9–10外部计算Python 先生成小图的轨道代表元与证书；Isabelle 实现 checker，并证明接受意味着覆盖、正确和无重复。
Week 11证明故障实验对自己的 theory 注入 lemma 删除、重命名、假设变化和 tactic 失效，记录失败目标、依赖和修复成本。
Week 12研究决策完成技术报告、可复现 artifact 和一次内部报告；与实验室老师讨论是继续数学 formalization，还是转入 proof repair / verification research。

7. 四定理应该怎样进入

不从“重新证明四定理”开始。 四定理涉及平面图、不可避免构型、可约性和大规模计算检查，直接进入会把学习时间消耗在既有工程上。

正确入口是证书体系。 AFP 已有可执行的平面性与非平面性证书检查器。先学习其“外部结果—证书—验证 checker—数学定理”架构，再研究群作用如何对称约化构型或着色搜索。

长期问题。 对称性约化后的构型集合是否完整？代表元是否唯一？外部枚举器若有 bug，Isabelle checker 能否拒绝错误证书？这比简单跑一个着色程序更接近可信数学研究。

8. 第一项可投稿研究：Verified Orbit Certificates

Working title

Verified Orbit Certificates for Symmetry-Reduced Finite Colorings

外部生成器按图自同构群作用生成着色轨道代表元；Isabelle checker 验证每个代表元合法、轨道覆盖完整、代表元之间不重复，并把检查结果连接到原始计数或穷举命题。

RQ1 · 数学与证书

怎样设计足够紧凑的轨道证书，使 checker 的 soundness 与 completeness 可以在 Isabelle 中证明？

RQ2 · 规模与约化

群作用约化能把不同图族的搜索空间减少多少？证书大小、生成时间和检查时间如何变化？

RQ3 · 证明工程

当定义、库依赖或证明策略变化时，结构化诊断能否比普通错误信息更快定位和修复失效证明？

RQ4 · AI 辅助

在相同上下文与尝试预算下，LLM 加 Isabelle 反馈能否修复群论 proof holes；哪些数学结构最容易造成错误建议？

两个互相支持、但不要混成一篇的发表出口

9. 与实验室老师讨论什么

第一次：工具与传统

请老师判断应优先使用 type class 还是 HOL-Algebra locale；了解实验室已有 Isabelle session、编码规范、可复用理论和构建方式。

第二次：数学边界

拿着项链与二面体着色 artifact，讨论群作用、Burnside 型计数和图自同构方向中真正存在的形式化缺口。

第三次：研究贡献

拿着证书 checker 与 proof-break 数据，判断贡献更适合形式化方法、软件工程还是纯数学合作。

必须避免

不要先说“想用 AI 证明大定理”。先展示可构建 theory、一个非平凡数学证明、一个可信 checker 和清楚的失败案例。

10. 十二周后的 Go / No-Go 标准

继续向数学深入：你愿意反复处理定义与表示，并能独立重建轨道—稳定子或 Sylow 证明中的关键部分。

转向 proof engineering：你对证明失败、依赖、自动化和修复的兴趣明显高于对新群论结论的兴趣。

形成双主线：你既能推进群作用形式化，又能从真实 proof failures 中提炼通用工具问题。这是最理想、也最符合你背景的结果。

暂停：十二周后仍只有阅读笔记，没有可构建 theory、checker 或可重复实验。此时应回到更接近现有软件可靠性工作的方向。

11. 核心资料，只按这个顺序读

  1. Isabelle2025-2 官方发行版：下载、版本和系统要求。
  2. Programming and Proving in Isabelle/HOL：第一、二周的主教材；重点是函数、归纳、自动化和 Isar。
  3. Archive of Formal Proofs：把它当作经过机械检查的研究档案，而不是代码片段仓库。
  4. Orbit–Stabiliser：群作用、轨道、稳定子和四面体旋转。
  5. Secondary Sylow Theorems：群作用如何进入更深的有限群论。
  6. Finitely Generated Abelian Groups：结构定理与大型代数 formalization 的组织方式。
  7. Representations of Finite Groups：Maschke、Schur 与表示论的长期入口。
  8. Planarity Certificates：学习可执行 checker、证书、soundness 与 completeness 的连接。

今天只做一件事：安装 Isabelle2025-2，跑通 Group_Warmup.thy，保存第一个可命令行构建的 session。不要先读四定理，也不要先调用 LLM 自动生成大段证明。