本期节目深入探讨 DeepSeek-AI 开源的 DeepSeek-Prover-V2 模型。我们讨论了它如何利用 DeepSeek-V3 进行子目标分解，结合强化学习，在 Lean 4 形式化定理证明中取得突破性进展，特别是在 MiniF2F 和 PutnamBench 等基准测试上的卓越表现，以及新引入的 ProverBench 和 AIME 问题的挑战。