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

数学定理证明，也能被 AI“无痛”拿下了？！

ingFang SC", Cambria, Cochin, Georgia, Times, "Times New Roman", serif;font-style: normal;font-variant-ligatures: normal;font-variant-caps: normal;font-weight: 400;letter-spacing: 0.75px;orphans: 2;text-align: justify;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(255, 255, 255);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">

ingFang SC", Cambria, Cochin, Georgia, Times, "Times New Roman", serif;font-style: normal;font-variant-ligatures: normal;font-variant-caps: normal;letter-spacing: 0.75px;orphans: 2;text-align: justify;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(255, 255, 255);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">671 B + MoE

ingFang SC", Cambria, Cochin, Georgia, Times, "Times New Roman", serif;font-size: 15px;font-style: normal;font-variant-ligatures: normal;font-variant-caps: normal;font-weight: 400;letter-spacing: 0.75px;orphans: 2;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(255, 255, 255);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">

关键指标	数据
总参数量	671 B（6710 亿）
架构	MoE，61 层 Transformer
隐藏维度	7 168
激活参数	≈ 37 B / token（稀疏激活）
上下文窗口	163 840 tokens （≈80 万汉字）
权重格式	BF16 +FP8量化可选

ingFang SC", Cambria, Cochin, Georgia, Times, "Times New Roman", serif;font-style: normal;font-variant-ligatures: normal;font-variant-caps: normal;letter-spacing: 0.75px;orphans: 2;text-align: justify;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(255, 255, 255);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">“数学天赋”从何而来？

模型直接在 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 个姿势开玩

Lean 4 自动补全

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

Math Agent

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

教材生成器

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

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

Lean 是什么？

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

把数学定理写成计算机能检查的“形式化证明”，再也不用担心证明里藏 bug；
写出带有“定理级”正确性保证的程序（证明即代码，代码即证明）；
做元编程：用 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 的关键升级点

速度
Lean 4 把前端 / 编译器整体重写，支持多线程解析 & 编译；大型项目（如 mathlib4）编译时间砍到 Lean 3 的一小段。
自举 + 单语言生态
编译器本身用 Lean 写→“吃自己狗粮”；扩展编译器、写宏、做插件再也不用切 Lua。
宏系统“类 Rust”
正规 hygienic 宏 + 语法扩展，写 DSL、证明 tactic、甚至给 Lean 加新语法，都像写普通 Lean 代码一样。
通用编程
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 可能会让专业研究者第一次认真思考：

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