主要证据
- Solving (some) formal math olympiad problemsS2 · 官方机构来源 · 官方公告 · 2022-02-02
OpenAI Lean 证明器通过专家迭代求解形式化奥赛题
该证明器在不同难度的形式命题上交替执行证明搜索与基于新发现证明的再训练。
发生了什么？
OpenAI 报告其基于 Lean 的 statement curriculum learning 在 miniF2F 上达到 41.2%，并自动证明若干 AMC/AIME 及两道改编 IMO 问题。
为什么重要？
它把语言模型定理证明与专家迭代结合，后者后来成为形式推理系统中的核心训练范式之一。
重要性说明：该工作展示了证明搜索与学习交替进行可以形成自举式课程，并在 miniF2F 上取得当时领先结果。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 神经证明器搜索 Lean 证明，并把成功证明作为新的训练数据。
- 人类贡献
- 研究者整理命题、设计专家迭代训练循环并评测生成的形式证明。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- lean-statement-curriculum-prover, lean
- 机构
- openai
- 数学问题
- minif2f, olympiad-mathematics
- 方法
- expert-iteration, proof-search, language-model
全部来源与工件
- Solving (some) formal math olympiad problemsS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-10
验证历史
- 2022-02-02 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
更正
当前没有记录的更正。