主要证据
- The Flyspeck Project repositoryS1 · 主要研究来源 · 代码仓库
- A formal proof of the Kepler conjectureS1 · 主要研究来源 · 论文 · 2015-01-09
Flyspeck 完成克卜勒猜想形式证明
完成后的工程同时形式化克卜勒猜想证明的数学文本与大型计算部分。
发生了什么？
Flyspeck 项目将 2014 年 8 月 10 日记录为完成日期；项目使用 HOL Light 与 Isabelle 构建克卜勒猜想形式证明，官方论文于 2015 年 1 月 9 日发布。
为什么重要？
Flyspeck 成为衡量复杂研究数学实现全面机器可检查所需规模、协作与工程能力的重要参照。
重要性说明：Flyspeck 的完成展示了：一个结合数百页数学文本与大量计算的超大型研究证明，可以被重构为由证明助手完整检查的形式工程。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 人机协作
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 符号
- AI 贡献
- 人类形式化者构建工程，HOL Light 与 Isabelle 执行可信证明检查与验证计算。
- 人类贡献
- Thomas Hales 与大型国际团队历时十余年形式化证明、数学库及计算验证组件。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- flyspeck, hol-light, isabelle
- 机构
- —
- 数学问题
- kepler-conjecture
- 方法
- formalization, proof-checking, verified-computation
全部来源与工件
- The Flyspeck Project repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
- A formal proof of the Kepler conjectureS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- Flyspeck formal proof repository工件 · 证明工件
验证历史
- 2014-08-10 · 尚属声明 · E3 · 可检查工件
Flyspeck 公开仓库记录项目完成日期并提供形式化工程。
- 2015-01-09 · 论文已发布 · E3 · 可检查工件
官方研究论文记录完成后的形式证明。E3 表示存在可检查 artifacts，并不意味着 Chronicle 独立重放整个工程。
更正
当前没有记录的更正。