AI 智能体 24 天形式化「巨大定理」

第 1 集 · Axiom 用 AI 智能体 24 天 Lean 形式化有限单群分类定理(2026-10-27,34 条)

Axiom Math 于 10 月下旬宣布完成有限单群分类定理（CFSG，绰号「巨大定理」）的首个完整机器校验证明：由数十个 AI agent 组成的集群在 24 天内，将这一约 15000 页、500 余篇论文、约 100 位数学家跨越数代人完成的人类史上最长数学证明，形式化为数千万行 Lean 代码，并由 Lean kernel 逐条逻辑验证。这是迄今规模最大的数学证明机器验证。

已确认

• Axiom 宣布完成 CFSG 的完整 Lean 自动形式化，为首个完整计算机校验证明，由 Lean kernel 逐条逻辑验证；定理内容为每个有限单群都属于素数阶循环群、交错群等已知类别，被称为「对称性的元素周期表」，是 20 世纪数学的重大成就之一。
• 原证明体量：约 15000 页、500 余篇论文、约 100 位数学家跨越数十年完成，散布于数千页期刊论文；据多个转发帖，40 多年来从未有数学家能独立核验。
• 形式化耗时 24 天，由数十个 AI agent 组成的集群完成；据 docdavkitty 相关转述，agent 通过 GitHub issues 和 Slack 协调分工、互相审查，瓶颈在验证而非生成。各帖对代码量说法不一，介于约 3800 万至 5000 万行之间，常见表述为 4310 万行或「超过 4300 万行」，构成迄今最大的 Lean 代码库之一。
• rohanpaulai 转述称过程中揪出 34 处错误；burnytech 转述称 AI 代理找出 5000 多处勘误但全部可修复；另有转述（含 FuSheng0306 帖）称发现并修复了原证明中存在数十年的一个漏洞。
• OpenAI 产品负责人 Kevin Weil 公开宣布该成果；Terence Tao 等人转发称赞。burnytech 等转发者指出该项目或成为规模最大的开源软件项目之一；此前 CFSG 一直被认为是最不可能被形式化的证明之一。
• Rutgers 数学教授 Alex Kontorovich 发帖转述 Timothy Gowers 的评价：鉴于 CFSG 证明的正确性历史上长期存在争议、散布上万期刊页而难以完全确认，其形式化完成是重大好消息。

尚未确认

• 精确代码行数在各帖间不一致（约 3800 万至 5000 万行）；「修复原证明数十年漏洞」「5000 多处勘误」与「34 处错误」等数字均来自转发者转述，未见原始技术报告佐证，彼此也可能指向不同口径。

为什么重要

• 「巨大定理」首次获得逐行机器验证。Gowers 与 Kontorovich 均指出，CFSG 因体量庞大、证明散布各处，其正确性长期无法完全确认，形式化验证为此提供了确定性背书，也顺带清理了原文献中数千处可修复瑕疵。
• 24 天完成人类数十年积累的证明验证，展示了 AI 智能体集群在大规模协作任务上的能力；有转发者指出此过程中验证而非生成才是真正瓶颈。有评论者认为这体现了 agent 群体协作模式的潜力，也有声音将其视为形式化验证可扩展到费马大定理、ABC 猜想等更多重大猜想的信号；还有发帖者（如 FuSheng0306）据此认为 AI 智能已超越人类数学水平。

• 约 1.5 万页有限单群分类定理完成 Lean 形式化，史上最大数学证明获机器验证 — eptwts · 2026-10-27
• Axiom 用 AI 智能体群完成史上最长数学证明的 Lean 形式化 — kevinweil · 2026-10-27
• 史上最大数学证明被机器验证：Axiom 用 Lean 完整形式化有限单群分类 — akorinek · 2026-10-27
• Axiom 24 天用 AI agent 集群形式化「巨大定理」，产出 4300 万行 Lean 代码 — rohanpaul_ai · 2026-10-27
• Agent 集群 24 天验证约 1.5 万页数学证明,还揪出十年老缺陷 — cneuralnetwork · 2026-10-27
• 人类史上最大数学证明获机器验证：有限单群分类定理完整 Lean 形式化 — stevenstrogatz · 2026-10-27
• 巨著定理被完全形式化，数学形式化再下一城 — IgorCarron · 2026-10-27
• 史上最大数学证明完成 Lean 机器验证：有限单群分类约 15000 页 — wellecks · 2026-10-27
• 迄今最大 Lean 代码库诞生，Szegedy：ABC 猜想若仍无法形式化将是明确信号 — ChrSzegedy · 2026-10-28
• 人类史上最大数学证明完成 Lean 形式化:4310 万行代码逐条机器验证 — pickover · 2026-10-28
• 史上最大数学证明获 Lean 全自动形式化:有限单群分类 1.5 万页 — PlisSergey · 2026-10-28
• AI 协作数周形式化数学最大定理:15000 页证明确认无误 — IgorCarron · 2026-10-28
• Axiom 用 Lean 完成有限单群分类定理的计算机自动形式化 — McDonaghMatthew · 2026-10-28
• Axiom 用 Lean 完整形式化有限单群分类定理，史上最大数学证明获机器验证 — GuillaumeLample · 2026-10-28
• 有限单群分类定理获完整 Lean 形式化，原证明达 15000 页 — Zulfikar_Ramzan · 2026-10-28
• Axiom 宣布人类史上最大数学证明完成 Lean 机器验证 — TheTuringPost · 2026-10-28
• AI agent 集群 24 天形式化 15000 页证明,Axiom 攻克「巨大定理」 — rickasaurus · 2026-10-28
• 史上最大数学证明获计算机验证:有限单群分类 Lean 化完成 — rickasaurus · 2026-10-28
• Axiom 用 AI 集群 24 天形式化史上最长数学证明:4310 万行 Lean 代码验证有限单群分类 — haider1 · 2026-10-28
• 史上最长数学证明被机器验证：Axiom 用 Lean 形式化 1.5 万页有限单群分类 — IgorCarron · 2026-10-28

还有 14 条相关讨论 →

第 2 集 · 有限单群分类定理完成 Lean 形式化(2026-11-03,2 条)

Axiom Math 团队宣布完成有限单群分类定理（CFSG）第一代证明的完整 Lean 形式化，每个逻辑步骤均由 Lean kernel 检查。项目规模约 4310 万行代码、205 万条声明，覆盖 715 篇论文与书籍、100 个里程碑。形式化过程中还审查出已发表论文中的多处证明问题，其中一处据称得到修正。

• 有限单群分类定理完成 Lean 形式化：4310 万行代码，还揪出已发表论文的一处证明问题 — ChrSzegedy · 2026-11-03
• 有限单群分类定理完成 Lean 形式化，4300万行代码揪出47篇论文96处错误 — ChrSzegedy · 2026-11-03