主要证据
- A Machine-Checked Proof of the Odd Order TheoremS1 · 主要研究来源 · 论文 · 2013-07-22
Coq 完成奇数阶定理的机器检查形式证明
项目在形式化定理本身的同时，建立了覆盖群论、线性代数、Galois 理论及实/复代数数的大规模数学库。
发生了什么？
ITP 2013 论文报告在 Coq 中完成 Feit–Thompson 奇数阶定理的完整构造性形式化，其证明只依赖 Coq 基础框架中的公理与规则。
为什么重要？
它显著提高机器检查研究数学所展示的规模与深度，并强化了后来可供自动化与 AI 系统使用的形式库基础设施。
重要性说明：历时六年的 Feit–Thompson 奇数阶定理 Coq 形式化展示了证明助手能够承载深层研究级数学论证，并同时建设有限群论、代数和数系等可复用形式库。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- 人机协作
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 符号
- AI 贡献
- 人类作者构造形式证明，Coq 按其基础规则检查每一步形式推理。
- 人类贡献
- 协作团队形式化数学内容、建设可复用形式库，并开发大型工程所需的证明方法与工具。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- coq
- 机构
- microsoft-research, inria
- 数学问题
- odd-order-theorem
- 方法
- formalization, proof-checking, mathematical-library
全部来源与工件
- A Machine-Checked Proof of the Odd Order TheoremS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2013-07-22 · 论文已发布 · E2 · 研究记录
ITP 同行评议论文记录了完整 Coq 形式化；machine_checked 表示由 Coq 完成验证，并不表示 Chronicle 独立重放全部工程。
更正
当前没有记录的更正。