主要证据
- Solution of the Robbins ProblemS1 · 主要研究来源 · 论文
EQP 找到解决 Robbins 猜想的证明
自动搜索在一个数十年未解决、长期接受人类与机器尝试的问题上产生了紧凑的等式推导。
发生了什么？
1996 年 10 月 10 日，William McCune 的 EQP 找到证明 Robbins algebra 为 Boolean algebra 的证明；随后该证明由 Otter 定理证明器检查并由数学家研究。
为什么重要？
该事件较早证明自动定理证明能够直接参与未解决数学问题，这也是现代 AI4Math 的核心目标之一。
重要性说明：EQP 对 Robbins algebra 的证明是自动定理证明器解决长期开放代数问题的标志性案例，展示 ATP 不仅可以重新证明已知命题，也能参与获得新的数学结果。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 新证明
- 接口
- 形式化, 符号
- AI 贡献
- EQP 自主搜索并找到形式证明；之后进行了独立的自动检查与人类数学审阅。
- 人类贡献
- William McCune 开发证明器与搜索设置；数学家对机器找到的证明进行解释、化简与传播。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- eqp, otter
- 机构
- argonne-national-laboratory
- 数学问题
- robbins-conjecture
- 方法
- equational-theorem-proving, automated-proof-search
全部来源与工件
- Solution of the Robbins ProblemS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 1996-10-10 · 论文已发布 · E3 · 可检查工件
Argonne 技术报告记录了 EQP 证明及后续 Otter 检查；machine checking 不意味着 Chronicle 自行裁决历史优先权。
更正
当前没有记录的更正。