刚刚，DeepSeek 在 Hugging Face 低调挂出 DeepSeek-Prover-V2-671B 模型仓库。
Sam Altman：？
这不是常规升级，而是一款专为数学定理证明打造的新物种；官方定位就是“Prover”——证明者。
671 B + MoE
|
|
|
|---|---|
|
|
671 B（6710 亿） |
|
|
|
|
|
|
|
|
|
|
|
163 840 tokens
|
|
|
|
稀疏 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），同时也是一门纯函数式编程语言。 -
能干什么： -
把数学定理写成计算机能检查的“形式化证明”，再也不用担心证明里藏 bug； -
写出带有“定理级”正确性保证的程序（证明即代码，代码即证明）； -
做元编程：用 Lean 给 Lean 本身写“宏”和自动化战术（tactic），让证明更省力。 -
幕后团队：
起家于 Microsoft Research（主作者 Leonardo de Moura），后来完全开源，学术界 + 民间社区（尤其是 mathlib 大佬们）一起把它推成了最火的证明助手之一。
Lean 4 又是什么？
一句话：Lean 4 = “Lean 的第四代内核 + 自举编译器 + 全能脚本语言”。
|
|
|
|
|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
飞起
|
|
|
|
纯 Lean 宏 + hygienic |
|
|
|
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 可能会让专业研究者第一次认真思考：
“定理证明，从此不用人类亲手上手了？！”
—— 以上就是目前能扒到的全部情报，更多信息，敬请期待！
（文：AGI Hunt）