主要证据
- Aristotle: IMO-level Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 2025-10-01
- Harmonic Aristotle IMO 2025 Lean proofsS1 · 主要研究来源 · 形式化工件
Aristotle 报告在 IMO 2025 上达到形式证明金牌等效水平
该架构生成并形式化有用引理、搜索形式证明，并通过专用组件处理几何。
发生了什么？
Aristotle 报告通过 Lean 证明搜索、非形式推理与专用几何求解器，在 IMO 2025 题目上达到金牌等效表现。
为什么重要？
它体现了集成式形式数学 Agent 的出现，而不只是单模型证明生成器。
重要性说明：Aristotle 将形式搜索、非形式引理生成与几何求解器整合，并报告达到 IMO 金牌等效水平。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 系统协调非形式推理、引理形式化、证明搜索与几何求解。
- 人类贡献
- 研究者构建集成架构并验证形式输出。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- aristotle, lean
- 机构
- harmonic
- 数学问题
- imo-2025
- 方法
- formal-proof-search, lemma-generation, geometry-solver
全部来源与工件
- Aristotle: IMO-level Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Harmonic Aristotle IMO 2025 Lean proofsS1 · 主要研究来源 · 形式化工件 · 访问于 2026-09-11
验证历史
- 2025-10-01 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。