主要证据
- A formal proof of the Kepler conjectureS1 · 主要研究来源 · 论文 · 2015-01-09
Flyspeck 启动克卜勒猜想长期形式化证明工程
项目计划同时形式化 Hales 证明中的书面数学论证与计算机计算部分，最终主要使用 HOL Light 与 Isabelle 完成。
发生了什么？
Thomas Hales 在 2003 年 1 月 15–18 日巴尔的摩 Joint Mathematics Meetings 上宣布 Flyspeck，目标是给出克卜勒猜想的完整形式证明；由于所引史料未保留具体宣布日，本条以会议开幕日作为 canonical 日期锚点。
为什么重要？
Flyspeck 后来成为大型证明助手工程的代表案例，展示形式系统能够端到端审计极其复杂的研究数学。
重要性说明：Flyspeck 将一个重要且高度依赖计算的数学证明验证问题转化为长期协作形式化工程，同时覆盖数学文本、计算过程与可复用证明助手基础设施。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 尚属声明
- 证据等级
- E2 · 研究记录
- AI 角色
- 人机协作
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 符号
- AI 贡献
- 人类主导形式化，证明助手执行可信推理、证明检查与大规模验证计算。
- 人类贡献
- Hales 与国际协作团队组织形式化、拆解原始证明，并实现形式库与验证流程。
- 验证状态
- 尚属声明 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- flyspeck, hol-light, isabelle
- 机构
- —
- 数学问题
- kepler-conjecture
- 方法
- formalization, proof-checking, verified-computation
全部来源与工件
- A formal proof of the Kepler conjectureS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- Joint Mathematics Meetings Baltimore 2003 programS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
验证历史
- 2003-01-15 · 尚属声明 · E2 · 研究记录
Flyspeck 官方发表记录说明 Hales 在 2003 年 1 月 Joint Mathematics Meetings 宣布该项目；AMS 档案确认会议日期为 1 月 15–18 日。
更正
当前没有记录的更正。