DeepSeek Prover-V2，这才是探索AGI 的正确姿势！
仅用于站内搜索，没有排版格式，具体信息请跳转上方微信公众号内链接
刚刚，DeepSeek在HuggingFace低调挂出DeepSeek-Prover-V2-671B模型仓库。
SamAltman：？
这不是常规升级，而是一款专为数学定理证明打造的新物种；官方定位就是“Prover”——证明者。
关键指标
数据
总参数量
架构
MoE，61层Transformer
隐藏维度
7168
激活参数
≈37B/token（稀疏激活）
上下文窗口
（≈80万汉字）
权重格式
BF16+FP8量化可选
稀疏MoE让它在“超大体型”与“可部署性”之间找到平衡——
真正吃满的参数只占~5.5%，推理成本比同级dense模型低得多。
Lean4生态深度绑定
模型直接在Lean4形式化证明框架上对齐训练，让输出一步到位就是可验证证明脚本。
海量合成+RL双加持
先是使用DeepSeek-Coder系模型生成自然语言讲解+Lean代码注释，扩大高质量数学语料库；
然后再用RLPAF/RMaxTS等强化学习策略做“自我博弈”，搜索更多证明路径。
超长上下文+MLA压显存
多头潜在注意力（MLA）一边把键值缓存压到极致，一边把上下文窗口拉到16万+，从而能将复杂定理也一次吞下。
miniF2F/ProofNet等数学基准据称再次刷新自家纪录（官方论文待放出）。
民间测试显示，利用kTransformers+减显存技巧，单张RTX4090就能跑流畅，显存降93%，吞吐提升5.7×。
MIT许可证：模型权重+代码全放出，可二创、可闭源部署，无附加条款。
HuggingFace直接下载163个分片即可起飞，也可走DeepSeekAPI/SambaNova等各家厂商的云端API使用。
如果你想本地化：
transformers+accelerate+cuda>=12.2，配8×H100或4090省流版，半天就能把你的教科书证明完。
由于Prover-V2在内部已有“证明链”，许多老派chain-of-thoughtprompt反而拖后腿。
社区开始实验“一句话任务描述即可”的新范式。
Lean社区掀起“让AI带我做作业”挑战，PhD候选人现场看模型把自己论文定理秒证，一脸复杂。
Lean4自动补全
VSCode+lean4-mode+Prover-V2后端，写一句sorry，模型给你整段证明。
MathAgent
让模型先把人类猜想翻译成Lean目标，再自己证明；Human只负责提问与最终sanity-check。
教材生成器
喂一本PDF《高等代数》，让Prover-V2自动生成“分步形式化证明+中文讲解”，瞬间把老师变助教。
另外，有必要科普一下——
定位：Lean是一个互动式定理证明器（InteractiveTheoremProver），同时也是一门纯函数式编程语言。
能干什么：
把数学定理写成计算机能检查的“形式化证明”，再也不用担心证明里藏bug；
写出带有“定理级”正确性保证的程序（证明即代码，代码即证明）；
做元编程：用Lean给Lean本身写“宏”和自动化战术（tactic），让证明更省力。
幕后团队：起家于MicrosoftResearch（主作者LeonardodeMoura），后来完全开源，学术界+民间社区（尤其是mathlib大佬们）一起把它推成了最火的证明助手之一。
一句话：Lean4=“Lean的第四代内核+自举编译器+全能脚本语言”。
特性
Lean3
Lean4
内核语言
C++
Lean本身（自举）
编译链
C++/Lua混合
单一Lean→C(或LLVM)
运行效率
OK
（10×级优化）
宏系统
tacticmonad+Lua
元编程库
tactic
用途
主要做数学
速度Lean4把前端/编译器整体重写，支持多线程解析&编译；大型项目（如mathlib4）编译时间砍到Lean3的一小段。
自举+单语言生态编译器本身用Lean写→“吃自己狗粮”；扩展编译器、写宏、做插件再也不用切Lua。
宏系统“类Rust”正规hygienic宏+语法扩展，写DSL、证明tactic、甚至给Lean加新语法，都像写普通Lean代码一样。
通用编程Lean4生成高效C代码，可直接写服务端、CLI工具；已经有人用它写游戏引擎、数据库原型。
严格可信：内核只有不到万行，所有证明最终都要过“审计关”；“只相信1万行小核心”比相信10万行编译器靠谱得多。
自动化友好：可以写tactic/AI代理让它自己填证明空白→DeepSeekProver、OpenAI“LeanGPT-f”都是这么玩的。
现代语法手感：有λ、patternmatching、依赖类型，“写证明像写代码，写代码顺便得到证明”。
Lean=给数学装上编译器；Lean4=给Lean本身插上涡轮。想玩自动化证明、形式化验证、或只是体验“写代码就能把定理证明了”的快感？Lean4就是当下最火的那把钥匙。
R2也要来了？
Reddit小道消息称DeepSeek还在憋一版“Research-2”升级，或许会把推理激活参数再砍一半、速度再翻倍。吃瓜群众，准备好🍿！
见NewDeepseekModelReleasedDeepSeek-Prover-V2-671B:r/accelerate
这次的DeepSeek-Prover-V2-671B，像是一次“把数学自动化”野心的实战验证。
相比于谄媚和娱乐，这次的DeepSeek选择了截然不同的方向。
——这才是探索AGI的正确姿势。
如果说ChatGPT让大众第一次感受生成式AI的魅力，那么Prover-V2可能会让专业研究者第一次认真思考：
“定理证明，从此不用人类亲手上手了？！”
——以上就是目前能扒到的全部情报，更多信息，敬请期待！
👇
👇
👇
另外，我还用AI进行了全网的AI资讯采集，并用AI进行挑选、审核、翻译、总结后发布到《AGIHunt》的知识星球中。
这是个只有信息、没有感情的AI资讯信息流（不是推荐流、不卖课、不讲道理、不教你做人、只提供信息）
