DeepSeek-Prover V1 用 800 万条合成 Lean statement+proof 数据把 whole-proof generation 推到新水平

DeepSeek-Prover 将自然语言竞赛数学问题自动翻译成 Lean 4 statements，过滤低质量 formalizations，再生成 proofs，构建约 800 万条 formal statement+proof 训练数据。基于 DeepSeekMath 7B 微调后，论文报告 miniF2F cumulative accuracy 约 52%，并在 Lean 4 FIMO benchmark 上证明 148 题中的 5 题，而 GPT-4 为 0。模型与 synthetic dataset 同步开放。