主要证据
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 2025-07-31
- Seed-Prover formal theorem-proving repositoryS1 · 主要研究来源 · 代码仓库
Seed-Prover 结合深度与广度形式推理并证明 IMO 2025 五道题
系统依据 Lean 反馈迭代改进整段证明，并使用深度与广度相结合的测试时搜索策略。
发生了什么？
Seed-Prover 报告证明 78.1% 的形式化历届 IMO 问题、超过一半 PutnamBench，并通过 Seed-Prover 与 Seed-Geometry 完成 IMO 2025 六题中的五题。
为什么重要？
它把形式奥赛证明从基准进展推进到几乎覆盖一届真实 IMO 题集。
重要性说明：Seed-Prover 展示了 Lean 验证的长程推理系统可以扩展到当届 IMO 大多数题目，并显著提升 PutnamBench 表现。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 证明器迭代修订整段 Lean 证明，专用几何引擎处理形式几何问题。
- 人类贡献
- 研究者设计推理策略、训练流程与几何引擎并评测形式证明。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- seed-prover, seed-geometry, lean
- 机构
- bytedance-seed
- 数学问题
- imo-2025, putnambench, minif2f
- 方法
- whole-proof-reasoning, lean-feedback, test-time-search
全部来源与工件
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Seed-Prover formal theorem-proving repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2025-07-31 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。