主要证据
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataS1 · 主要研究来源 · 论文 · 2024-05-23
DeepSeek-Prover 用数百万合成形式命题扩展 Lean 定理证明
自然语言竞赛题被翻译为 Lean 陈述、过滤、搜索证明，再作为合成训练数据回流。
发生了什么？
DeepSeek-Prover 在包含约 800 万条带证明形式命题的合成语料上训练，并报告 Lean 4 miniF2F 累计 52% 的证明率以及 5 道 FIMO 证明。
为什么重要？
该工作确立了“合成形式数据生成”作为扩展神经定理证明器的重要路线。
重要性说明：DeepSeek-Prover 展示了大规模合成 Lean 数据能够显著提升整段形式证明生成能力。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 模型生成形式命题与整段证明，由 Lean 进行机械检查。
- 人类贡献
- 研究者设计翻译、过滤、证明生成与训练管线。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- deepseek-prover, lean
- 机构
- deepseek
- 数学问题
- minif2f, fimo
- 方法
- synthetic-data, whole-proof-generation, lean
全部来源与工件
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
验证历史
- 2024-05-23 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
更正
当前没有记录的更正。