最近有个消息值得所有做 AI 应用和 AI 辅助科研的人停下来看一眼OpenAI 的推理模型针对某个数学猜想输出了一份完整证明结果提交给数学家后24 小时内就被驳回了。驳回理由很有代表性——AI 确实证对了每一句话但那份证明已经和原猜想无关了。这句话信息量很大。它把 LLM 生成内容最典型的病状一次性说清楚了局部句子全部成立整体目标完全跑偏。自然语言里这叫跑题代码里这叫实现错了需求数学证明里就是证明了一个与原命题无关的定理。更深一层它暴露出一个关键问题AI 生成的证明在形式上可能非常流畅、逻辑上局部自洽但模型在语义层面并没有真正理解自己在证明什么。这篇文章围绕这个事件做一次技术拆解不吹不黑重点回答三个问题AI 生成数学证明的工作流到底是什么样为什么会出现每句话都对、整体却无关的现象如果你自己要用 AI 辅助定理证明应该怎么验证、怎么规避同类问题。这个主题和 OpenAI Codex 的走红是绑在一起的——Codex 作为代码智能体已经能完成不少工程任务但代码有编译器和测试用例兜底数学证明的验证要比这严格得多也更容易暴露 LLM 的局部正确陷阱。1. AI 数学证明核心工作流速览先把这套流程涉及的核心模块和验证工具列出来方便对照你手头已有的环境看缺什么。模块作用典型代表大语言模型推理生成证明步骤、补全引理、提出证明思路GPT 系列、o 系列推理模型、Codex 智能体代码/证明生成把自然语言思路翻译成形式化证明脚本OpenAI Codex、DeepSeek-Prover 等形式化证明助手校验每一步逻辑是否严格成立Lean 4、CoqRocq、Isabelle数学库提供已证定理和定义供证明引用MathlibLean、stdlibCoq自动化策略自动补全证明中的 gap 和显然步骤aesop、omega、linarith、ring、simp人工复核评估证明是否与原猜想匹配、是否有数学价值数学家、领域审稿人如果只是把 AI 当灵感生成器只需要一个能聊数学的大模型如果目标是让 AI 产出可验证的严格证明那至少需要大模型 证明助手 数学库三件套。这次 OpenAI 的证明被快速驳回大概率就是因为在三件套里跑通了生成和逻辑校验但缺失了最关键的人工目标校验。证明助手只负责检查证明对不负责回答这是不是你要证明的东西。2. 事件复盘数学家在 24 小时内到底看到了什么数学家拿到一份 AI 生成的证明后不会像普通读者那样逐行欣赏而是会先做三件事看目标、看引理、看依赖。这次驳回能发生在 24 小时内说明问题不是藏在某个复杂计算里而是出在证明的骨架层面。第一看它声称证明了什么。如果 AI 声称证明了 X 猜想那证明文本的前几行就必须出现 X 猜想的严格定义并且最终定理的陈述必须和原猜想在逻辑上等价。这一步看着简单实际是 AI 最容易翻车的地方。模型可能在证明过程中偷偷替换了假设条件把一个带约束的命题改成了无约束版本也可能把一个存在性命题证成了构造性命题甚至可能重新定义了一个看起来很像、但逻辑上并不等价的猜测。第二检查证明目标是否在过程中发生漂移。完整的数学证明是一个目标驱动的长链条每一行都应该为最终命题服务。AI 在生成过程中很容易把一个辅助引理当成主命题或者把推导过程中的中间结论误认为题目要求。比如它可能花了大量篇幅证明了一个更强的命题但这个更强命题本身就是错的或者证明了一个更弱的命题而这个更弱命题无法推出原猜想。从材料看这次被驳回的核心原因就是证明已经与原来的猜想无关本质上就是目标漂移。第三挑几个关键引理做独立性检查。一份证明里通常嵌套多个引理每个引理看上去都有证明但如果某个引理本身就包含了原猜想的等价形式那就等于循环论证整个证明实际没有任何推进。数学家会单独把证明中新建引理列表拉出来逐一确认它们是否是社区已经证明过的结论还是 AI 自己发明的断言。数学家之所以能在 24 小时内驳回恰恰说明问题足够结构性。如果只是某个引理的计算细节出错24 小时未必够用但证明的命题与原猜想无关这种骨架级错误几乎一眼就能看出来根本不需要读完所有细节。3. 为什么 AI 会证对每句话却离题万里这是全文技术含量最高的一节可以从模型机制、验证机制、语义理解三个层面拆开看。3.1 Token 预测机制天然偏向局部大语言模型的生成逻辑是逐 token 预测下一个最可能的符号推理模型内部会做更长的思维链搜索但本质上仍然是基于上下文做下一段最可能的内容。这个机制决定了它擅长补全局部步骤擅长把上一步到下一步的衔接做得像模像样但不擅长维护一个跨几千步的全局目标。数学证明恰恰是强目标驱动的每一行都必须服务于最终命题。模型在长证明里非常容易发生目标漂移——写着写着把一个辅助命题当成主命题把引申出来的结论当成题目要求。每一行和上一行之间的自然语言过渡都很顺滑但整条链的头部和尾部已经分家了。这就是为什么 AI 生成的证明经常出现前面在证 A后面在证 B但每一句话读起来都成立的荒诞效果。3.2 局部自洽不等于全局正确人类数学家构造证明时脑子里有一个骨架先证明引理 A再通过 A 构造 B主动绕开 C 里的困难。大模型没有这种规划能力它靠的是海量数学论文和教科书语料训练出来的模式记忆知道什么情况下该写因此令由于但这些语言习惯不能替代逻辑约束。当模型生成的第 50 行出现一个小目标偏差第 100 行、第 200 行会顺着这个偏差继续推导最终得到一个自洽的平行宇宙证明。平行宇宙里的每一步都对但整个宇宙已经不是原猜想的宇宙了。更麻烦的是如果没人提醒模型自己很难发现这个偏差因为它生成的每一步都是基于上一步的最优延续局部上没有任何异常信号。3.3 形式化验证能拦截逻辑错误拦截不了语义漂移有人会问如果 AI 输出的是 Lean 4 代码Lean 不是会严格检查类型和逻辑吗为什么还会出现每句话都对、整体无关这里的关键在于Lean 只负责检查你写出的定理声明是否被严格证明它不负责检查这个声明是不是你想证明的那一个。如果 AI 在 Lean 里声明了一个稍微不同的定理比如把对所有自然数成立写成了对无穷多个自然数成立Lean 不会报错它会老老实实验证这个更弱命题的证明。形式化工具解决的是逻辑严谨性问题解决不了目标一致性问题。目标一致性需要一个外部的裁判这个裁判目前只能是人。换句话说Lean 可以拦住证错了但拦不住证的不是这个题。3.4 语义理解与研究动机的缺失更深一层的问题在于数学证明不只是逻辑链条还包含为什么这条路能走通的直觉。顶尖数学家看到一个新证明会关心它的方法有没有推广价值、是否揭示了更深的结构、能不能用来解决相邻问题。AI 生成的证明即使逻辑完全正确也可能因为冗长、不自然、缺乏方法美感而被认为没有数学价值。这次 OpenAI 的证明被驳回很可能不只是逻辑层面出问题还有数学意义的缺失。一个证明如果只是机械地把一个命题改写成另一个等价但更复杂的命题对数学社区没有任何增量那即使形式化验证通过也不会被接受。数学研究的终极目标是理解而理解这件事目前还不在 LLM 的能力范围内。4. AI 辅助数学证明的常用工具链如果你不满足于看热闹想自己试一下 AI 辅助数学证明下面这套工具链是当前社区里比较主流的组合。这里只写通用思路具体版本号和安装命令以官方仓库为准。4.1 底层模型OpenAI Codex 与推理模型Codex 是 OpenAI 的编码智能体它不止能写业务代码也能在 Lean/Mathlib 仓库里完成补全、重构、加引理等任务。Codex 的 harness 已经开源可以在 GitHub 上找到仓库。它的工作方式偏 agent拿到一个数学目标会拆解成多个子任务调用文件读取、代码搜索、编译验证等工具迭代尝试。实际使用时很多人会让 Codex 打开一个 Lean 项目告诉它证明某某引理它会在项目中生成中间文件、声明定理、尝试编译并根据 Lean 的报错信息反复修改。这已经比单纯在对话框里要一个证明靠谱得多因为每一步都有编译器的即时反馈。4.2 证明助手Lean 4 MathlibLean 4 是目前形式化数学社区最活跃的证明助手配套的 Mathlib 数学库里已经沉淀了大量数论、代数、分析、组合的已证定理。AI 生成的证明脚本可以直接导入 Mathlib引用已有结论避免重复劳动。Lean 的安装和管理主要靠 elan 和 lake 两个工具类似于 Rust 生态里的 rustup 和 cargo。下载 Mathlib 通常需要几个 G 的空间首次编译耗时也比较长建议提前准备。4.3 其他形式化平台如果研究方向偏逻辑或程序语言Coq现在也叫 Rocq是常见选择Isabelle/HOL 在分析、代数领域有比较成熟的自动化工具对 AI 生成证明的容错度会高一点。不过从 AI 工具适配程度看Lean 社区和 GitHub 上的 AI for Math 项目更活跃参考资料也更多。4.4 自动化策略库在 Lean 里AI 写完一部分证明后剩下的显然简单计算往往要交给自动化策略处理。常见的有linarith处理线性算术omega处理 Presburger 算术ring、norm_num处理多项式与数值计算aesop通用自动化搜索simp化简这些策略不是拿来就能用的需要导入对应库。AI 如果能把这些策略调用得当证明的生产效率会高很多。5. 环境准备与最小验证流程如果没有现成的 AI 辅助证明环境这里给一套通用检查清单按顺序做能少踩不少坑。5.1 前置检查操作系统Linux 或 macOS 最省心Windows 可以用 WSLPython 版本如果要用 OpenAI API 写脚本建议 Python 3.10 以上Lean/elan/lake按 Lean 官方指引安装注意 PATHMathlib用lakefile管理依赖首次拉取会比较大API Key调用 OpenAI 接口需要合法账号和配额按官方申请流程操作磁盘空间预留 10G 以上Mathlib 依赖和构建缓存都比较占空间。5.2 启动 Lean 项目# 创建 Lean 项目命令以官方模板为准 lake init my_proof cd my_proof lake update lake build上面命令只是通用模板具体依赖声明需要在lakefile.toml里写清楚。5.3 让 AI 生成证明写一个 Python 脚本把 Lean 中的定理声明发给大模型让它尝试生成by ...后的证明部分。这是一个比较常见的使用模式import openai client openai.OpenAI(api_keyyour-api-key) prompt 给定 Lean 4 中的定理声明 theorem example_square (n : ℕ) : n^2 n n * (n 1) 请给出 Lean 4 的完整证明脚本要求使用的引理均来自 Mathlib。 response client.chat.completions.create( modelgpt-4o, # 按实际可用模型调整 messages[{role: user, content: prompt}], temperature0.2, max_tokens2000 ) print(response.choices[0].message.content)注意这里的模型名和接口样例只是示意实际要以你账号能使用的模型为准。长证明生成任务优先选推理能力更强的模型。5.4 用 Lean 验证把 AI 返回的证明脚本写进Test.lean然后运行lake env lean Test.lean如果没有报错说明证明在逻辑上通过了 Lean 的检查。注意这只是通过了逻辑一致性检查不代表证明的就是原猜想。你还必须把证明最顶部的 theorem 声明和你真正想证的目标逐字比对。6. 验证清单如何在收到 AI 证明后快速发现问题参考数学家 24 小时驳回的做法任何人收到一份 AI 证明都应该按下面这套清单做目标一致性审计。6.1 目标声明比对把 AI 证明里的最终定理声明单独提出来与原始猜想逐词比对约束条件有没有变少或变多量化范围有没有变弱比如对所有自然数改成对充分大的自然数充分条件和必要条件的方向有没有反有没有偷偷引入新定义导致证明对象本质上是另一个问题这一步最重要也最容易看出 AI 的问题。很多 AI 证明的 bug 就藏在一个看似不起眼的限定词里。6.2 依赖审查看证明用到了哪些关键引理。如果发现某个引理和原猜想强度相当甚至本身就是原猜想的另一个表述那就基本可以判定存在循环论证。人工复核时可以这样做把用到的所有引理名打印出来逐一确认它们是否都已经被社区证明过还是 AI 在声明里自己创造的。6.3 构造可执行的反例测试如果一个证明最终断言了对所有 X 成立立刻找几个具体的 X 代进去看结论是否成立。AI 写出来的证明经常会在特殊值上露馅比如 0、1、空集、负无穷这些边界。这个方法特别适合批量验证如果有多个 AI 生成的证明可以写脚本自动替换参数跑一小批实例做快速筛选。6.4 独立复现最可靠的验证是让第二个模型或者第二个人独立重新证明一遍而不是在同一个证明上修修补补。独立证明如果走向完全不同的路线那原证明至少不像看起来那么显然。6.5 交给领域专家最终判定权还是在人手里。因为数学证明不仅要求正确还要求有意义、有清晰的研究动机。专家觉得这个证明没有任何可推广技术时即使逻辑无误也可能被判定为无价值证明。AI 可以作为候选手稿的生成器但不能作为最终裁判。7. 批量任务与接口能力AI 参与数学证明的另一个常见场景是批量补全引理一个大型 Lean 库里可能有几百个sorry未完成的证明占位AI 可以逐个生成候选证明再统一跑 Lean 验证。7.1 批量流程设计输入Lean 项目里所有带 sorry 的定理 ↓ 分批发送给大模型限制并发和 token 消耗 ↓ 把生成的证明写回对应文件 ↓ 统一执行 lake build ↓ 收集失败项和报错信息进入下一轮7.2 批量调用示例import time from openai import OpenAI client OpenAI(api_keyyour-api-key) lemmas [ {name: lemma_A, statement: theorem lemma_A : ...}, {name: lemma_B, statement: theorem lemma_B : ...}, ] results [] for item in lemmas: try: resp client.chat.completions.create( modelgpt-4o, messages[ {role: system, content: 你是一个 Lean 4 证明助手只输出证明脚本。}, {role: user, content: f请证明{item[statement]}}, ], temperature0.2, max_tokens1500, ) results.append({ name: item[name], proof: resp.choices[0].message.content, }) except Exception as e: results.append({name: item[name], error: str(e)}) time.sleep(1) # 避免请求过于频繁 for r in results: print(r)7.3 API 接入注意点并发与限流先读官方限流说明避免批量任务触发 429成本控制长证明的 token 消耗很高建议先小批量测试并设置max_tokens上限失败重试遇到超时或网络抖动用退避重试策略访问范围如果部署了本地 API 代理或推理服务应限制在内网访问不要暴露到公网。8. 资源占用与性能观察AI 做数学证明不是开销小的任务。它虽然不像图像生成那样依赖大显存但推理模型的上下文窗口和生成长度对算力消耗同样明显。8.1 长证明的 token 消耗一个中等难度的 Lean 证明AI 生成的完整脚本可能几百到几千 token如果模型还输出思维链实际消耗会翻倍甚至更多。批量处理几百个引理时API 账单会涨得很快。建议先在单个定理上摸清平均 token 成本再决定批量的规模。8.2 本机验证的计算开销Lean 验证本身对 GPU 没有硬性要求主要吃 CPU 和内存。Mathlib 这种大型库在首次构建时会长时间高负载运行建议给足内存例如 16G 以上同时关闭其他大型应用。如果使用 WSL还要注意磁盘 IO 性能。8.3 显存占用如果你的环境是在本地跑一个小模型生成证明比如量化版本的 7B 级模型显存占用通常在 6G 到 8G 量级具体取决于模型、上下文长度和量化方式。更稳妥的判断是不同模型差异很大实际占用以本机nvidia-smi或任务管理器的实测为准。如果显存不够就把模型量化等级调低或者改用云端 API。8.4 观察指标生成阶段看请求耗时、token 速度、失败率验证阶段看 Lean 编译耗时、内存峰值、是否触发 OOM迭代阶段看平均几轮能修过一个sorry。这些指标没有统一标准但可以给自己的项目建立一套基线后续用来对比模型版本或策略升级的效果。9. 常见问题与排查方法问题现象可能原因排查方式解决方案AI 返回的证明在 Lean 里大量报错模型输出的是伪代码或自然语言混排检查开头是否包含代码块标记要求模型只输出 Lean 脚本或改用 Codex 直接操作仓库Lean 报 unknown identifier缺少 Mathlib 导入或依赖没装好查看报错位置是否在 import 区补全import Mathlib先执行lake update证明能编译但审阅发现和原题无关目标声明在生成过程中被改写把 theorem 声明和原猜想逐字比对做目标一致性审计必要时冻结定理声明后再生成反复出现循环论证模型直接引用了目标定理本身检查依赖引理列表审查引理依赖闭包禁止 AI 引用目标定理API 请求 429触发限流或并发过高查看返回头里的 retry-after增加间隔、降低并发或升级配额Mathlib 首次构建太久依赖多、磁盘 IO 慢查看 CPU 和 IO 占用换 SSD、关闭安全软件或使用预构建缓存批量任务到一半卡住单次请求超时或网络断裂查看任务日志和异常增加超时重试任务设计成断点续跑AI 生成的证明步骤看似流畅但缺少关键一步模型把显然当成合法推理人工阅读证明关键跳步把显然位置单独标记交给自动化策略补全10. 最佳实践与合规边界工程层面有几个建议可以直接用。第一永远先小规模测试。不要一上来就让 AI 证明一个未解决的猜想先让它证明数学库里已有的定理对比它生成的证明和标准证明之间的差异。这样既能验证工具链也能摸清模型的风格和常见错误模式。第二冻结目标声明。在提示词里让模型只输出证明脚本不要修改 theorem 声明可以在工程上减少目标漂移。更进一步可以在 Lean 文件里预先写好 theorem 声明并显式标注sorry让 AI 只补证明部分不允许改声明。第三把生成和验证分开成两个流水线。生成节点可以失败验证节点必须严格。两者分离后你随时可以替换更强的模型或更严格的验证器而不会互相污染。第四做好日志和版本管理。每个 AI 生成的证明都要记录模型版本、提示词版本、Lean 版本、验证结果。数学证明讲究可复现这些信息缺一不可。第五如果要在论文、课程或公开项目中使用 AI 生成的证明要明确学术机构的披露政策。AI 可以被用作辅助工具但署名、结果正确性、创新性责任仍然在人。公开发布 AI 生成的证明前必须由具备资质的数学工作者复核并明确声明 AI 参与程度。涉及版权材料时不要把未经授权的论文全文、私人未发表手稿塞给 AI 做生成输入注意隐私与版权边界。本文提到的所有工具和接口都应在测试环境中按官方许可使用。11. 总结与下一步这次AI 证明被 24 小时驳回的事件最大的价值不是嘲讽某个模型而是把局部正确不等于全局正确这件事摆到了台面上。对做 AI 工程的人来说这是一个非常典型的范式模型输出流畅、局部自洽、表面上完成度高但在目标一致性这个层面失守了。数学证明不过是把这个问题暴露得最彻底的一个场景同样的坑在自动代码生成、长文档写作、数据分析结论里一样存在。如果你接下来想跟进这个方向建议按下面顺序做。第一搭一套 Lean Mathlib 的最小环境把手头的简单定理跑通。不需要 GPU普通笔记本加 16G 内存就够起步。第二让 AI 在一个明确定理上生成证明再按第 6 节的验证清单做一次完整审计。重点看目标声明有没有漂移、引理依赖有没有循环。第三选一个数学库里有sorry的定理做批量补全实验记录成功率、失败原因和成本。这一步能帮你建立对 AI 数学证明能力的真实判断而不是停留在宣传话术层面。第四重点关注目标一致性和依赖循环两个指标它们比 Lean 编译是否通过更能衡量 AI 证明的真实质量。遇到问题也不难排查多看看 Lean 报错信息多保留中间产物。AI 数学证明这个方向还在快速迭代OpenAI Codex 和开源证明助手都在持续更新今天复杂的流程过几个月可能就有更顺手的工具替代。先把验证方法论练好工具怎么换都不慌。建议收藏备用等你真的开始用 AI 做数学证明时回来按这套清单跑一遍。