主要证据
- A computer-checked proof of the Four Colour TheoremS1 · 主要研究来源 · 论文
Coq 完整检查四色定理形式证明
该形式化把组合论证与计算机分类检查都纳入 Coq，使正确性依赖通用证明助手验证机制，而非四色定理专用外部程序。
发生了什么？
至 2005 年 4 月 21 日，Georges Gonthier 的“A computer-checked proof of the Four Colour Theorem”报告已公开传播，其中描述了由 Coq v7.3.1 完整检查的成功形式化证明。
为什么重要？
它成为大型计算机辅助证明可以转化为可审计机器检查数学的标志性示范。
重要性说明：Gonthier 的 Coq 工程展示了：一个此前高度依赖定制计算的著名定理，可以被重构为同时覆盖数学论证与计算部分的完整机器检查形式证明。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- 人机协作
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 符号
- AI 贡献
- 人类设计形式证明工程，Coq 执行并检查全部形式逻辑与计算步骤。
- 人类贡献
- Georges Gonthier 设计并实现形式化、证明脚本、tactics 与数学编码。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- coq
- 机构
- microsoft-research
- 数学问题
- four-colour-theorem
- 方法
- formalization, proof-checking, verified-computation
全部来源与工件
- A computer-checked proof of the Four Colour TheoremS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- Four Color Theorem Verified in CoqS3 · 独立学术来源 · 社区来源 · 访问于 2026-09-15
验证历史
- 2005-04-21 · 论文已发布 · E2 · 研究记录
原始报告明确说明证明由 Coq 完整检查；带日期的独立公开记录确认该报告至迟于 2005 年 4 月 21 日已经公开。
更正
当前没有记录的更正。