DeepSeek 在數學定理證明領域推出了專用模型 Prover-V2，目標是用 AI 在 Lean 4 形式化驗證系統裡自動證明數學定理。
這個方向為什麼重要？
數學定理證明是 AI 能力的一個極端測試場。因為數學不接受「差不多對」——證明要麼完全正確，要麼就是錯的。不存在「95% 正確的證明」這種東西。
形式化驗證系統（例如 Lean 4）會像編譯器檢查語法一樣檢查每一步推理邏輯。一步不對，整個證明就報錯。這對 AI 的邏輯推理能力是最嚴格的考驗。
Prover-V2 的表現
在 miniF2F 基準測試上，Prover-V2 拿到了接近或達到當前最優的成績。它採用的方法是子目標分解——把複雜證明拆解成一系列更小的子目標，逐個攻破。
這和人類數學家的思路很像：面對一個難題，先想「要證明 A 成立，我需要先證明 B 和 C，而證明 B 又需要先確認 D……」
與通用推理模型的區別
通用模型（GPT、Claude、Gemini）做數學推理靠的是 Chain-of-Thought——本質上是「用自然語言一步步推」。這種方式對簡單問題效果不錯，但複雜證明很容易在某一步出現邏輯漏洞。
Prover-V2 走的是形式化路線，每一步都有 Lean 4 驗證。好處是不存在「幻覺」，壞處是適用範圍很窄——只能在形式化系統裡工作。
意義
數學定理證明是一個看起來很小眾但影響深遠的方向。如果 AI 真的能在形式化系統裡可靠地證明複雜定理，那它可以被應用到軟體驗證、硬體驗證、密碼學證明等一系列關鍵領域。
DeepSeek 在這個方向上的投入說明他們不只是在卷通用大模型的基準測試——也在認真佈局基礎科學工具。
參考來源：CocoLoop、DeepSeek Prover-V2 論文