先看这次的争议事件OpenAI 的 AI 系统声称攻破了一个数学猜想结果 24 小时内就被数学家驳回。驳回理由非常典型——AI 生成的证明里每一句话单看都像是正确的推理但整套推导早就偏离了原猜想。换句话说它不是“证明错了”而是“证明的根本不是同一个东西”。这不是数学领域的孤立问题。做代码生成、做 AI Agent 的人应该都很熟悉这个场景模型生成的代码能编译、单个函数看起来也正确但拼在一起根本没有实现需求。AI 数学证明踩的是同一个坑只是数学对全局一致性的要求更严格所以暴露得更快。这篇文章不会去争论“AI 到底能不能做数学”而是把它当作一个工程问题来分析为什么大模型容易“局部正确、整体跑偏”如何用 Lean 这类形式化验证工具判断 AI 证明是否真的有效普通程序员和科研人员在做 AI 辅助推理时怎样才能避免被流畅的“伪证明”带偏。下面会先给一套 AI 证明验证方案的能力速览然后从问题根因、形式化验证流程、反例检查、流水线配置、算力开销、排查清单和最佳实践几个维度展开。如果你关心 ChatGPT 类模型、Codex 这类 AI Agent 在科研和编程里的真实边界这篇可以直接收藏。1. AI 数学证明验证方案与能力速览能力项说明核心问题AI 生成的证明可能在局部成立但整体偏离原始猜想推荐验证方式用 Lean / Isabelle / Coq 等形式化证明助手检查证明步骤验证原理证明助手要求每一步推导都满足类型规则无法通过编译即不成立工具类型交互式定理证明器Lean 4 目前社区最活跃主要能力判定证明是否形式有效、生成可复现的 proof script、定位错误步骤适用环节数学证明、算法正确性验证、安全协议验证、AI 生成代码的正确性检查不适用场景结论无法形式化表达、或只有模糊文本描述时验证成本极高启动方式命令行执行lean或 VS Code 安装 Lean 扩展是否支持批量任务支持可通过脚本对多个.lean文件批量编译检查是否支持接口 APILean 本身不提供 HTTP API但可被 Python/Node 脚本调用适合读者AI 研究者、算法工程师、数据分析师、理工科科研人员这套方案的核心思路并不复杂不要相信 AI 输出的“证明文本”而是把证明转成一种机器可检查的语言。如果 AI 生成的证明能通过 Lean 的形式化检查至少说明证明过程在逻辑上是严密、可复现的如果不能那不管文字看起来多有道理都只能当作思路提示不能当作结论。2. 为什么 AI 会“证对每一句话却跟原猜想无关”先拆一下这个现象背后的原因。大语言模型本质上是逐 token 生成文本的。模型在每一步都在做“下一个最可能的 token”预测它擅长的是续写出一段“看起来像数学证明”的文本而不是对一个数学目标进行全局规划。数学证明恰恰是一个强结构对象每个中间结论必须由前面的公理和已证引理推出最终结论必须精确命中原始命题。问题就出在这里。当证明很长时模型可能已经丢失了最初的约束。它会在某个子问题上反复推导把另一个容易被证明的命题当作目标甚至悄悄替换定义。从局部的任何一句话看推理似乎没有明显毛病但从整体看证明链已经断裂目标已经漂移。数学家能 24 小时驳回很大程度就是因为最终结论和原猜想根本不是同一个命题。这种“目标漂移”在代码生成里同样常见。OpenAI 的 Codex 这类编码 Agent 在解决复杂 issue 时也可能生成大量“能编译但不对题”的代码。原因一致模型在长上下文里逐渐把“完成用户需求”替换成了“完成一个类似的中间任务”。所以AI 证明被驳回不该被当成笑话它暴露的是当前生成式模型的一个通用短板局部连贯性很强全局一致性很弱。另外一个容易被忽略的点是模型在生成证明时不会主动做否定性检查。人类数学家会反复尝试构造反例来推翻自己但大模型默认的工作模式是顺着文本继续生成。它很少主动说“这里有个反例所以证明不成立”。这也是为什么让 AI 独立完成完整证明非常危险——它天然缺少证伪倾向。3. 如何快速判断 AI 证明是否有效形式化验证先跑起来3.1 Lean 环境准备判断 AI 证明是否有效最可靠的办法是把它形式化。Lean 4 是目前数学界使用最多的定理证明器之一社区贡献了大量数学库比如 Mathlib。它的工作方式是你把命题、定义和证明步骤写进一个.lean文件Lean 编译器会逐行检查类型是否正确、每一步推导是否符合逻辑规则。环境准备可以按下面的顺序来。如果你用 VS Code直接安装 Lean 4 扩展最省事如果习惯命令行可以安装 Lean 的对应版本然后直接执行lean命令。安装完成之后可以在项目目录下建立一个ProofTest.lean文件先把最小可运行的验证跑通。# 检查 lean 是否安装成功 lean --version # 直接编译检查某个 .lean 文件 lean ProofTest.lean # 如果使用 Lake 管理 Lean 项目可以这样创建和运行 lake new demoproof cd demoproof lake build3.2 一个最小 Lean 验证示例下面是一个最简单的 Lean 证明示例。它的目标是对任意自然数 n证明n 0 n。如果你自己写数学证明会用“加法定义右侧为 0”之类的理由Lean 里直接调用simp策略就能完成。-- 最小示例证明 n 0 n theorem add_zero_example (n : Nat) : n 0 n : by simp这个例子看起来很简单但它说明了验证的本质Lean 不会因为这句话“读起来顺”就接受它必须判断n 0和n在定义层面是否定义相等。现实中的数学证明当然要复杂得多但验证的框架是一样的——把每一步推理写清楚交给机器检查。3.3 用 AI 生成 Lean 证明草稿很多使用 OpenAI 模型做数学的人已经在尝试这样一条链路先让模型用自然语言写一个证明思路再让模型把思路转成 Lean 代码最后用 Lean 编译器验证。这个流程里OpenAI 的模型只是“草稿生成器”Lean 才是“裁判”。下面是一段 Python 脚本的示意用来调用 OpenAI 兼容接口生成 Lean 证明草稿并保存为.lean文件。注意实际使用时需要根据你手上的模型服务调整接口地址和参数。这个流程本身也适用于本地部署的开源模型不一定要绑定某一家厂商。import os # 假设你有一个 OpenAI 兼容的 API 服务 from openai import OpenAI client OpenAI( api_keyos.environ.get(OPENAI_API_KEY), base_urlos.environ.get(OPENAI_API_BASE, https://api.openai.com) ) prompt 把下面的数学证明改写成 Lean 4 代码。 请只输出 .lean 文件内容不要输出解释。 命题对任意自然数 n有 n 0 n。 response client.chat.completions.create( modelgpt-4o, messages[{role: user, content: prompt}], ) lean_code response.choices[0].message.content # 去掉可能包裹的 markdown 代码块 lean_code lean_code.replace(lean, ).replace(, ) # 保存文件并用 lean 检查 with open(generated_proof.lean, w, encodingutf-8) as f: f.write(lean_code) os.system(lean generated_proof.lean)这段脚本的核心价值在于它把不可靠的“语言描述”转换成了可执行的验证命令。如果lean generated_proof.lean没有报错证明至少在形式上是有效的如果报错就把错误信息返回给模型让它重新修改。这种“生成-验证-反馈”循环比直接让 AI 给一个自然语言证明要可靠得多。4. 目标一致性检查先反驳再相信形式化验证能证明“推理步骤合法”但它不能完全替代人工判断“这是不是原问题要的结论”。这次事件里的关键问题——AI 证明的结论已经偏离原猜想——就是目标一致性检查要解决的问题。4.1 反例搜索脚本在把证明形式化之前可以先做一轮更便宜的反例搜索。比如如果猜想是针对某个自然数性质的你可以写一个暴力枚举脚本在小范围内寻找反例。这一步能快速过滤掉大量“看似有道理但根本站不住脚”的结论。下面是一个 Python 反例搜索模板实际使用时要替换成你自己的命题和条件函数def conjecture(n: int) - bool: # 示例某个未被证伪的猜想 # 这里只是一个占位逻辑请替换为实际命题 return n * n % 2 0 or n % 2 0 def find_counterexample(limit: int 10000): for n in range(1, limit): if not conjecture(n): return n return None counterexample find_counterexample() if counterexample is not None: print(f发现反例{counterexample}) else: print(f在 1 到 9999 范围内未发现反例但不能证明命题成立)注意没有发现反例不等于证明成立只是说明在采样范围内没被推翻。反例搜索适合做第一道筛选不能作为最终结论。4.2 检查目标是否漂移目标漂移是这次被驳回事件里最核心的问题。在工程上也可以像代码验收一样去检查“实现是否满足原始需求”。具体要做好三件事第一把原始猜想完整地抄写到验证文件里。不要把“AI 自己复述的版本”当目标很多目标漂移就是模型在复述时偷换了条件。要让 AI 从原始文本里重新抽取命题并和人工核对。第二把证明里最终得到的结论单独抽出来和原始命题逐项对比。变量是否一致约束条件是否一致是否存在额外假设比如原猜想说的是“所有偶数”AI 证明最后可能只证明了“所有平方数”这种差别通过逐项对比可以很快发现。第三把 AI 生成的证明拆成若干独立引理分别验证。大模型经常在一个长证明里隐藏跳步。拆成若干个lemma之后编译器能告诉你哪一个引理没有被证明或者哪一个引理和最终目标无关。这是定位“哪一步开始跑偏”的最有效手段。5. 可落地的 AI 辅助科研验证流水线5.1 流水线架构把上面的思路整合起来就形成了一条可复用的“AI 生成-自动验证-人工复核”流水线。它不只是针对数学证明也可以迁移到 AI 辅助代码生成、算法设计等场景。流水线分为四个阶段。第一阶段让 AI 生成自然语言证明思路或者代码第二阶段使用 Lean/Isabelle 等工具做形式化验证第三阶段用反例搜索和小规模测试做快速筛选第四阶段由人工检查目标一致性。一句话总结就是AI 负责生成可能正确的结果机器负责检查形式正确性人负责确认目标匹配度。5.2 流水线配置与命令假设你有一个批量验证需求比如要检查 20 个由 AI 生成的引理证明可以用一个简单的配置文件来控制输入目录、输出目录、验证工具和是否开启反例搜索。pipeline: input_dir: ./ai_proofs output_dir: ./verified_proofs formal_tool: lean4 counterexample_search: true search_limit: 100000 log_file: ./logs/verification.log配合上面的配置可以用一个批量检查脚本读取目录下所有.lean文件并依次执行编译检查。下面是一个简化的 shell 示例#!/bin/bash for file in ./ai_proofs/*.lean; do echo checking $file lean $file || echo FAIL: $file done如果验证失败把失败信息丢回给 AI 模型让模型尝试修改再重新验证。这种“反馈循环”是当前 AI 辅助证明里最实际的用法。它能显著减少人工逐行检查的工作量但不能完全替代人工判断——因为 Lean 只能保证证明形式有效不能保证你最初选的命题就足够贴切。6. 算力开销与性能观察讨论 AI 数学证明时算力开销是绕不开的话题。要把一条完整的证明流水线跑起来至少涉及两部分开销第一是调用大模型生成证明草稿的推理开销第二是 Lean 编译器做形式化检查的计算开销。大模型推理的开销取决于你选择的模型规模和 API 定价。如果你用云端 API成本直接与输入输出的 token 数挂钩证明越长费用越高。如果你在本地用开源模型显存占用和推理速度会直接决定验证循环的迭代效率。更稳妥的判断是先在短命题上跑通全流程再逐渐增加命题复杂度不要一上来就让模型生成一个超大证明。Lean 编译验证的算力开销相对较低大多数场景在普通 CPU 上就能完成。但如果证明文件很大或者引入了庞大的 Mathlib 依赖首次构建会花不少时间。实际占用需要以本机测试为准不过一般来说形式化验证环节的硬件门槛低于大模型推理环节。可以从几个维度观察性能模型首 token 延迟、完整生成耗时、Lean 编译时长、迭代轮数。建议在流水线里加入时间戳和日志记录方便定位瓶颈。如果发现模型频繁生成错误代码需要调整提示词或换更强的模型如果发现 Lean 编译慢则要考虑拆分子证明减少单次编译规模。7. 常见问题与排查方法问题现象可能原因排查方式解决方案AI 生成的证明看似完整但被专家驳回推理链存在跳步或最终结论偏离原始命题最后结论和原始命题逐项对比拆成多个 lemma 分别验证使用 Lean 形式化验证对每个引理单独检查Lean 编译报类型错误AI 生成的证明里变量替换错误、类型不匹配查看编译器报错位置检查定义是否被提前替换把报错信息返回给 AI要求重新生成对应片段证明对象是自然语言文本无法直接形式化问题本身缺少严格定义或形式化成本过高先建立形式化定义再生成证明把问题拆小先证明可形式化的关键引理反例搜索没有发现反例但证明仍不成立反例搜索范围有限或命题本身在更大范围内存在反例扩大搜索范围或使用更复杂的搜索策略把反例搜索作为第一步筛选不能作为最终判断依据API 调用超时或失败模型推理时间过长、网络不稳定、上下文过长检查 API 日志、拆分长 prompt、增加超时时间缩短 prompt分批处理加入重试机制批量验证任务卡住某个.lean文件陷入长时间编译或者模型生成死循环检查日志、限制单文件最大编译时间增加超时设置跳过异常文件并记录日志AI 生成的证明附带额外假设模型在推理过程中加入了原猜想没有的条件将证明里所有局部假设列出和原始条件对比明确禁止模型引入未给定条件人工终审8. 最佳实践与合规提醒基于这类事件可以总结出几条工程化建议适用于所有涉及 AI 推理、代码生成和数学证明的场景。第一把 AI 定位成“候选生成器”不是“结论验证器”。所有 AI 生成的结果都先进入验证流程而不是直接采用。验证方式可以是 Lean 这类形式化工具、反例搜索、独立实现对比等。第二保留最小可运行验证配置。环境搭建完成一次后要记录依赖版本、命令和配置避免下次重建环境时踩坑。Lean 版本和 Mathlib 版本之间的兼容性问题很常见建议把版本锁进项目配置。第三AI 生成证明的过程要留痕。记录输入 prompt、模型生成内容、验证结果、修改轮次这些日志不仅能帮助复现问题也是科研可复现性的基本要求。第四注意版权与科研诚信。AI 生成的内容可能来自训练数据中的已有论证发布前需要确认是否涉及他人未公开成果不能直接拿 AI 生成的证明当作原创结论。涉及受版权保护的论文、代码、数学库时注意遵守对应的开源协议和引用规范。第五商用或发表前进行人工复核。形式化验证能证明逻辑有效性但研究成果的学术价值、创新性和准确性仍然需要研究者负责。尤其当 AI 结论涉及姓名、机构、模型评价时要避免误导性表述。9. 总结这次事件最值得记住的一句话是AI 生成的证明第一步不是相信而是验证。它能在一段长文本里生成“每一步都像正确”的推导但它同样会悄悄偏离目标最终证明一个和原猜想无关的命题。如果你看完这篇想自己试一次建议从一件小事开始选一个你已经知道正确结论的简单命题让 AI 生成完整证明然后用 Lean 做一次形式化验证。这个流程能让你直观感受到“自然语言上的正确”和“形式化验证上的正确”之间的差距。最容易踩的坑是看到 AI 输出了一段逻辑通顺的证明文本后就默认它已经完成了证明。所有绕过机器验证和反例检查的“证明”都只能当作猜想。后续值得关注的方向有两类。一类是 AI 证明生成器和形式化验证工具的深度整合未来模型可以直接输出可验证的 proof script而不是自然语言证明另一类是更强的目标一致性检测方法帮助模型在长推理中保持对原始命题的追踪。对科研人员和工程师来说尽早建立“AI 生成 机器验证 人工复核”这套工作习惯会比单纯讨论模型能力提升更有实际价值。