DeepSeek在数学定理证明领域搞了个专用模型Prover-V2，目标是用AI在Lean 4形式化验证系统里自动证明数学定理。
这个方向为什么重要？
数学定理证明是AI能力的一个极端测试场。因为数学不接受”差不多对”——证明要么完全正确，要么就是错的。不存在”95%正确的证明”这种东西。
形式化验证系统（比如Lean 4）会像编译器检查语法一样检查每一步推理逻辑。一步不对，整个证明就报错。这对AI的逻辑推理能力是最严格的考验。
Prover-V2的表现
在miniF2F benchmark上，Prover-V2拿到了接近或达到当期最优的成绩。它用的方法是子目标分解——把复杂证明拆成一系列更小的子目标，逐个攻破。
这和人类数学家的思路很像：面对一个难题，先想”要证明A成立，我需要先证明B和C，而证明B又需要先确认D……”
和通用推理模型的区别
通用模型（GPT、Claude、Gemini）做数学推理靠的是Chain-of-Thought——本质上是”用自然语言一步步推”。这种方式对简单问题效果不错，但复杂证明很容易在某一步出现逻辑漏洞。
Prover-V2走的是形式化路线，每一步都有Lean 4验证。好处是不存在”幻觉”，坏处是适用范围很窄——只能在形式化系统里工作。
意义
数学定理证明是一个看起来很小众但影响深远的方向。如果AI真的能在形式化系统里可靠地证明复杂定理，那它可以被应用到软件验证、硬件验证、密码学证明等一系列关键领域。
DeepSeek在这个方向上的投入说明他们不只是在卷通用大模型的benchmark——也在认真布局基础科学工具。
参考来源：DeepSeek Prover-V2论文