DeepSeek Prover-V2，这才是探索AGI 的正确姿势！

Sam Altman：？

这不是常规升级，而是一款专为数学定理证明打造的新物种；官方定位就是“Prover”——证明者。

671 B + MoE

稀疏 MoE 让它在“超大体型”与“可部署性”之间找到平衡——

真正吃满的参数只占 ~5.5 %，推理成本比同级 dense 模型低得多。

“数学天赋”从何而来？

Lean 4 生态深度绑定

模型直接在 Lean 4 形式化证明框架上对齐训练，让输出一步到位就是可验证证明脚本。

海量合成 + RL 双加持

先是使用 DeepSeek-Coder 系模型生成自然语言讲解 + Lean 代码注释，扩大高质量数学语料库；

然后再用 RLPAF / RMaxTS 等强化学习策略做“自我博弈”，搜索更多证明路径 。

超长上下文 + MLA 压显存

多头潜在注意力（MLA）一边把键值缓存压到极致，一边把上下文窗口拉到 16 万+，从而能将复杂定理也一次吞下。

miniF2F / ProofNet 等数学基准据称再次刷新自家纪录（官方论文待放出）。

民间测试显示，利用 kTransformers + 减显存技巧，单张 RTX 4090 就能跑流畅，显存降 93%，吞吐提升 5.7×。

开源 & 商用策略

MIT 许可证：模型权重 + 代码全放出，可二创、可闭源部署，无附加条款 。

Hugging Face 直接下载 163 个分片即可起飞，也可走 DeepSeek API / SambaNova 等各家厂商的云端API 使用。

如果你想本地化：

transformers + accelerate + cuda>=12.2，配 8×H100 或 4090 省流版，半天就能把你的教科书证明完。

由于 Prover-V2 在内部已有“证明链”，许多老派 chain-of-thought prompt 反而拖后腿。

社区开始实验“一句话任务描述即可”的新范式。

Lean 社区掀起“让 AI 带我做作业”挑战，PhD 候选人现场看模型把自己论文定理秒证，一脸复杂。

3 个姿势开玩

VS Code + lean4-mode + Prover-V2 后端，写一句 sorry，模型给你整段证明。

让模型先把人类猜想翻译成 Lean 目标，再自己证明；Human 只负责提问与最终 sanity-check。

喂一本 PDF《高等代数》，让 Prover-V2 自动生成“分步形式化证明 + 中文讲解”，瞬间把老师变助教。

另外，有必要科普一下——

Lean 是什么？

• 定位：
  Lean 是一个 互动式定理证明器（Interactive Theorem Prover），同时也是一门纯函数式编程语言。
• 能干什么：

1. 把数学定理写成计算机能检查的“形式化证明”，再也不用担心证明里藏 bug；
2. 写出带有“定理级”正确性保证的程序（证明即代码，代码即证明）；
3. 做元编程：用 Lean 给 Lean 本身写“宏”和自动化战术（tactic），让证明更省力。

• 幕后团队：
  起家于 Microsoft Research（主作者 Leonardo de Moura），后来完全开源，学术界 + 民间社区（尤其是 mathlib 大佬们）一起把它推成了最火的证明助手之一。

Lean 4 又是什么？

一句话：Lean 4 = “Lean 的第四代内核 + 自举编译器 + 全能脚本语言”。

特性	Lean 3	Lean 4
内核语言	C++	Lean 本身（自举）
编译链	C++/Lua 混合	单一 Lean→C (或 LLVM)
运行效率	OK	飞起 （10× 级优化）
宏系统	tactic monad + Lua	纯 Lean 宏 + hygienic
元编程库	tactic	Lean.Elab, Lean.Meta
用途	主要做数学	数学 + 工程代码 + 脚本

3 到 4 的关键升级点

1. 速度
   Lean 4 把前端 / 编译器整体重写，支持多线程解析 & 编译；大型项目（如 mathlib4）编译时间砍到 Lean 3 的一小段。

2. 自举 + 单语言生态
   编译器本身用 Lean 写→“吃自己狗粮”；扩展编译器、写宏、做插件再也不用切 Lua。

3. 宏系统“类 Rust”
   正规 hygienic 宏 + 语法扩展，写 DSL、证明 tactic、甚至给 Lean 加新语法，都像写普通 Lean 代码一样。

4. 通用编程
   Lean 4 生成高效 C 代码，可直接写服务端、CLI 工具；已经有人用它写游戏引擎、数据库原型。

数学界和工程界的最爱

• 严格可信：内核只有不到万行，所有证明最终都要过“审计关”；“只相信 1 万行小核心”比相信 10 万行编译器靠谱得多。
• 自动化友好：可以写 tactic / AI 代理让它自己填证明空白→DeepSeek Prover、OpenAI “Lean GPT-f” 都是这么玩的。
• 现代语法手感：有 λ、pattern matching、依赖类型，“写证明像写代码，写代码顺便得到证明”。

一句话总结

Lean = 给数学装上编译器；Lean 4 = 给 Lean 本身插上涡轮。
想玩自动化证明、形式化验证、或只是体验“写代码就能把定理证明了”的快感？Lean 4 就是当下最火的那把钥匙。

One More Thing…

R2 也要来了？

Reddit 小道消息称 DeepSeek 还在憋一版“Research-2”升级，或许会把推理激活参数再砍一半、速度再翻倍。吃瓜群众，准备好?！

见 New Deepseek Model Released DeepSeek-Prover-V2-671B : r/accelerate



https://www.reddit.com/r/accelerate/comments/1kbc78w/new_deepseek_model_released_deepseekproverv2671b/

这次的DeepSeek-Prover-V2-671B，像是一次“把数学自动化”野心的实战验证。

相比于谄媚和娱乐，这次的DeepSeek 选择了截然不同的方向。

——这才是探索AGI 的正确姿势。

如果说 ChatGPT 让大众第一次感受生成式 AI 的魅力，那么 Prover-V2 可能会让专业研究者第一次认真思考：

“定理证明，从此不用人类亲手上手了？！