OpenAI公开数学证明：4款开源AI数学工具本地就能跑

OpenAI近期公开了一项引人关注的成果：内部一个新模型在一个月内解决了100多道长期未决的数学开放问题，并用Lean这类形式化证明语言，把最难的Navier-Stokes（视频中称"Neville Stokes"）相关问题的证明完整开源，放到了GitHub上。这次开源与以往闭门造车式的"我们做到了"不同——证明代码全公开、形式化验证脚手架也开源、第三方可以独立验证。

对普通开发者、学生和数学爱好者来说，更实际的信息是：一批不依赖内部模型、消费级显卡就能跑的开源AI数学工具同步可用。本文把其中四款工具的定位、能力和硬件门槛一次讲清楚，方便你按需选择。

OpenAI 开源了什么

据B站UP主的梳理，OpenAI在官方公告中提到，内部新模型一个月内搞定了100多道数学难题，并用Lean形式化语言写出了可被机器独立验证的证明。这次开源同时发生了三件事：

证明代码全部公开，可以直接参考和复用；
形式化验证的脚手架（scaffolding）也一并开源，任何第三方都能独立跑一遍验证；
一批开源项目（Lean Copilot、DeepSeek^广告-Math类模型、OpenProver等）同步可用，不需要OpenAI的内部模型，消费级显卡即可运行。

OpenAI的Neville Stokes

这里最关键的一点，是"形式化验证"这一金标准。AI写出的数学证明必须经过Lean内核逐步验证，写到 sorry（跳步占位符）等于0、报错等于0，才算真正没有跳步、全部步骤都成立。这套标准连OpenAI自己都遵循，也是判断一个AI证明是否"靠谱"的核心依据。

形式化证明语言 Lean 是由微软研究院开发的定理证明器与函数式编程语言，目前主流版本为 Lean 4。与普通数学写作不同，Lean 要求每一个推导步骤都以机器可检查的方式显式声明，由内核逐步验证其逻辑正确性。Mathlib 是 Lean 社区维护的数学库，收录了数万条已被形式化验证的定理和引理，相当于 Lean 世界里的"数学百科全书"。sorry 关键字是 Lean 提供的占位符，允许作者暂时跳过某个子目标继续编写，但编译时会产生警告——因此 sorry = 0 意味着证明中没有任何未完成的步骤，是衡量形式化证明完整性的黄金指标。Navier-Stokes 方程是描述流体运动的偏微分方程组，其光滑解的存在性与唯一性是七大"千禧年大奖难题"之一，悬赏百万美元至今未解，OpenAI 此次针对的是该方程的特定相关问题而非完整的千禧年问题本身。

四款工具，定位完全不同

虽然都围绕"AI+数学证明"，但这四款工具的用途差异很大，搞清楚定位才能避免选错。

OpenAI Navier-Stokes 证明仓库

这是直接对应OpenAI公开的千年难题级证明的代码库，在GitHub趋势榜排名靠前，约1856颗星，采用Apache 2.0协议。仓库基于 Lean 4.34 加上 Mathlib 数学库构建。

最值得看的指标是 sorry = 0、报错为0，意味着没有任何跳步，所有证明步骤都被Lean内核独立验证过。想本地跑很简单：Clone仓库后编译即可，硬件要求约8G内存加5G硬盘（用于缓存Mathlib）。这适合想直接研究或复用顶级证明代码的研究者。

Lean Copilot：给Lean的AI助手

Lean Copilot由Lean开发相关团队出品，是一个内嵌在Lean IDE里的AI证明助手，有三个核心能力：

战术建议（tactic suggestion）：当你写到 by sorry 卡住时，AI推荐可用的证明战术；
证明搜索：让大模型与传统自动证明器（如ESAP类工具）协同搜索多步证明；
前提选择（premise selection）：当证明目标涉及Mathlib库时，AI帮你找出可能有用的引理。

Lean Copilot的三个核心能力

它对硬件相对友好：CPU就能跑，如果借助本地大模型需要约8G内存；若走云端API则几乎零门槛。适合已经在用Lean写证明、希望提效的程序员和工程师。

DeepSeek-Math 7B：开源数学大模型

这是一款7B参数的开源数学大模型，可以直接对话求解高等数学题。在数学竞赛类基准（MATH）上，其RL强化学习版本加上工具调用能达到约60%的准确率，接近GPT-4的水平，超过部分对标模型；7B规模却能跑出接近Minerva级别的成绩，性价比突出。

7B模型接近Minerva水平

Hugging Face上提供三个版本：Base预训练版、Instruct对话版、RL强化学习版。硬件门槛在四款里最低：FP16需要约16G显存（如4090、A100级别），4位量化后8G显存的3060就能跑。对预算有限的学生和想试水的工程师尤其友好。

MATH 基准（Hendrycks Math）是学术界广泛使用的数学评测集，涵盖代数、几何、数论、组合、微积分等竞赛级题目，共 12500 道，难度从 AMC 到 AIME 不等，满分为 100%。Minerva 是 Google 于 2022 年发布的数学专用大模型（基于 PaLM 微调），在 MATH 上曾创下当时最优成绩，是衡量数学模型性能的重要参照基线。RL（强化学习）版本指通过过程奖励或结果奖励对模型进行强化学习微调，使其在解题时更倾向于输出可验证的正确步骤，而非仅生成"看起来合理"的文本。**4位量化（4-bit quantization）**是一种模型压缩技术，将模型权重从16位浮点数压缩为4位整数表示，可将显存占用降低约75%，代价是略微损失精度，但对推理任务影响通常可接受，使得原本需要A100的模型能在消费级3060显卡上运行。

OpenProver：自动跑证明的Agent系统

OpenProver由布拉格查理大学（Charles University）团队发布，并被CICM会议收录。它采用 Planner–Worker–Verifier 三段式Agent架构：

Planner 负责拆解证明任务；
Worker 并行尝试多种证明方法；
Verifier 用Lean 4内核自动验证，证明错误就退回Planner重做，正确才保留。

OpenProver的Planner重做机制

它的三大亮点是可复现的评估、交互式终端，以及基于ProofNet的研究级基准。用于研究级问题时，能力比Lean Copilot更强，但门槛也更高，更适合有一定基础的研究者。

CICM（Conferences on Intelligent Computer Mathematics） 是形式化数学与自动推理领域最重要的学术会议之一，收录意味着 OpenProver 的方法经过了同行评审。ProofNet 是一个专为形式化数学证明设计的研究级基准数据集，题目来源于本科至研究生水平的数学教材，难度远超竞赛题，是评估自动证明系统上限能力的标准测试集。Planner–Worker–Verifier 架构本质上是一种"计划-执行-验证"的多智能体循环：Planner 将复杂证明目标拆解为子目标，Worker 并行探索多条证明路径，Verifier 充当裁判——这种设计允许系统在失败后自动回溯重试，而不依赖人工干预，是当前 AI 辅助定理证明领域的主流范式之一。

怎么选？按角色对号入座

综合来看，四款工具可以按使用者身份快速匹配：

学生党：选 DeepSeek-Math，硬件门槛最低、直接对话就能解题；
程序员/工程师：选 Lean Copilot，深度嵌入Lean开发流程、提效明显；
想看顶级证明：直接看 OpenAI 的 Navier-Stokes 证明仓库；
研究即用：选 OpenProver，Agent自动化搜索证明能力更强。

上手成本也不高：OpenProver约30分钟能跑起来，DeepSeek-Math五行Python即可调用，Lean Copilot加两行依赖就能集成。

为什么这件事值得关注

这波开源真正的意义，不在于"AI又解了几道题"，而在于它把"可验证"放在了核心位置。数学证明和自然语言生成不同，对就是对、错就是错，Lean内核会无情地拒绝任何跳步或漏洞。AI给出的每一步都要过机器验证这一关，这让"AI做数学"从演示走向了可信。

对个人用户而言，这些工具全部开源免费、消费级硬件可跑，意味着形式化数学证明的门槛正在快速下降。无论是解高数题、写论文公式，还是研究前沿难题，都能找到对应趁手的开源方案。

（本文信息来源为B站UP主对OpenAI官方公告及各项目README的整理，数据截至相关公告发布时。部分专有名词以视频口述音译为准，如Navier-Stokes、Mathlib等，实际使用时请以官方仓库为准。）