最近一个和“AI 推翻百年数学猜想”相关的话题在数学圈和程序员社区同时炸开了锅。一份看起来既有 AI 参与、又经过了 Lean 证明助手“验证过”的数学证明在同行复核时被发现有隐藏漏洞原本已经准备庆祝的研究氛围瞬间冷静下来。我真正想讨论的问题不是“AI 能不能写数学证明”而是一个更尖锐的问题一套经过程序库逐行检查的证明为什么还能被找出漏洞如果你的第一反应是“那肯定是 AI 乱写”这篇文章可能尤其适合你。因为这里面的真正问题比“AI 乱写”要微妙得多也和我们日常写的单元测试、静态检查、类型系统有很强的可比性。读完这篇文章你会理解Lean 究竟校验了什么、没校验什么一个“通过了机器验证”的证明为何仍可能不是原猜想的证明以及如果你自己想把 AI 生成的证明用于安全敏感或数学严谨场景应该走哪几步排查流程。1. 为什么“AI 证明一打就假”值得开发者关注这件事最具冲击力的一点不是 AI 生成的数学证明本身错了而是“经过形式化验证工具检查过”的证明也会被推倒。很多人下意识地认为机器验证 正确。如果机器验证过的结果都不可信那我们还能信什么把它换成我们更熟悉的场景就理解了你写了一段代码单元测试全部通过。静态检查也没有报错。CI 部署到生产环境。然后用户反馈数据算错了。问题往往出在测试用例没有覆盖真实场景或者业务需求本身被理解错了。代码“执行正确”不代表“业务正确”。数学证明里的情况完全一样。Lean 这类形式化验证工具保证的是“在给定的形式系统内证明的每一步推导都符合规则”。但它不会自动知道你写的定理是否真的等价于你想证明的那个数学命题。所以这次争议暴露的并不是 Lean 本身不可靠而是AI 生成证明 形式化验证”这个新流程里存在一个巨大的语义中间层这个中间层几乎没有人专门去负责审查。把这件事当作一次技术事件来复盘对开发者有直接借鉴意义。尤其是正在做 AI Agent 可靠性、自然语言生成代码、安全关键系统验证的人这篇文章里讲的绝大多数问题都会以另一种形式出现在你的项目里。2. 基础概念Lean、AI 自动定理证明与“证明漏洞”2.1 Lean 是什么它检查的到底是什么Lean 是一个交互式定理证明器最新版本是 Lean 4由微软研究院和卡内基梅隆大学等机构的研究者主导开发。它和 Coq、Isabelle/HOL 属于同一代工具核心思想是把数学证明拆成极小步的推理交给一个非常小的内核kernel检查。这个“极小内核”是理解 Lean 的关键。你可以把内核想象成一个极其严格的编译器它只认固定的几条推理规则。所有高级策略、自动化工具、AI 生成的代码最终都要化简成内核可以接受的原始步骤。如果某一步不合法内核会直接拒绝。所以Lean 解决的是传统数学论文中“这里显然成立”这种省略带来的隐患。它不让任何一步跳过检查。但它也有边界。Lean 只能证明你写出来的定理不能证明你脑子里想的那个定理。只要定理陈述写错后面的证明再严谨也只是在严谨地证明一个错误命题。2.2 AI 自动定理证明的两种路径AI 参与定理证明目前主流有两种路径第一种是让 LLM 直接生成形式化证明代码。比如给一个大模型一个 Lean 定理目标让它输出策略代码然后交给 Lean 执行。如果 Lean 接受这道题就算完成了。第二种是自动形式化。让 LLM 把人类语言写成的数学命题翻译成 Lean 中的形式化定理陈述。这看起来只是“翻译”实际上是最容易出问题的环节。数学自然语言充满歧义和上下文依赖同一个词在不同分支学科含义可能完全不同。两种路径可以组合使用。AI 先做翻译再写证明步骤最后通过 Lean 编译形成一条完整的自动证明流水线。这也是这次争议事件中很可能采用的流程。2.3 “证明漏洞”可能出现在哪个环节在 AI Lean 的工作流里漏洞可能出现在四个不同的层级层级负责内容漏洞风险问题陈述层把自然语言猜想转成形式化命题高语义翻译容易出错定理层定理声明是否在形式上合法低编译能检查语法证明层证明是否完整闭合没有使用sorry中容易隐蔽公理层证明依赖了哪些底层公理中依赖不一致会让结论失真很多人只盯着“证明层”认为编译通过就等于没问题。但真正的争议往往出在“问题陈述层”和“公理层”。这也是这次新闻里“证明被验证过却又被推翻”的技术原因。3. 一次“验证通过”的证明为什么还会翻车把这次争议放到更大的背景里看它并不是孤例。任何一个 AI 辅助的数学证明要真正成立需要同时满足三个条件定理陈述与原命题等价。证明过程完整无洞。依赖的公理集合可以被目标领域接受。任何一个条件没满足都会出现“验证通过但证明无效”的情况。3.1 定理陈述并不等价最典型的错误是原命题说“对所有自然数都成立”形式化时变成了“对所有小于某个上界的自然数都成立”。这种错误在自动形式化中很常见因为 LLM 在翻译时可能受到训练数据里相近模式的影响把“充分大”理解成“所有大于 100 的数”或者把“整数”理解成“正整数”。Lean 会告诉你这个定理在形式系统内成立了。但它不会告诉你这个定理不是你想证的那个。3.2 公理集合隐含不一致第二个常见问题是公理层面的差异。原猜想是在某一套数学基础如 ZFC 集合论下提出的而 Lean 使用类型论作为基础并且在库中默认引入了命题外延、函数外延、选择公理等。如果一个证明大量依赖Classical.choice选择公理但原猜想要求的是构造性证明那么即使 Lean 验证通过这个证明在构造数学的语境下也没有价值。更有风险的是自定义公理。如果项目里出现了一行axiom my_axiom : False那么整个系统就会变不一致之后可以证明任何命题包括荒谬的命题。这种“任何命题都能证”的状态从逻辑上说是完全崩塌的。3.3 证明里有未闭合的洞第三个常见问题是证明本身有洞却没有被发现。Lean 里有一个专门用来“暂时跳过目标”的策略sorry。如果你写theorem fake_proof : ∀ n : Nat, n 1 n : by intro n sorryLean 在默认状态下会编译通过但会输出一个警告declaration uses sorry。对一个大型项目来说如果大家对警告不敏感这类虚假定理就会悄悄混进代码库。更麻烦的是AI 在生成证明代码时经常使用sorry来填进度。如果没有人仔细检查构建日志这些洞就会保留在最终产物里。3.4 版本与环境漂移最后还有版本问题。Lean 以及它的数学库 mathlib4 更新很快。同一个定理在不同版本的库中可能一个能证明另一个不能。如果你想复现别人的“AI 证明”却使用了不同版本的 Lean 或 mathlib得到的结果可能完全不同。所以一个严谨的 AI 证明项目必须锁定 Lean 版本和 mathlib 版本否则“验证通过”本身就是一个不可复现的临时状态。4. 用 Python 体验“看起来对”与“真正证明”的差距在进入 Lean 实操之前先用我们最熟悉的 Python 做一个对照实验体会一下“有限验证”与“数学证明”的区别。假设我们想验证一个简化版哥德巴赫猜想每个大于等于 4 的偶数都可以表示为两个素数之和。我们写一个循环把从小到大的偶数都检查一遍def is_prime(n): if n 2: return False for i in range(2, int(n ** 0.5) 1): if n % i 0: return False return True def check_goldbach_upto(limit): checked 0 for n in range(4, limit 1, 2): found False for p in range(2, n): if is_prime(p) and is_prime(n - p): found True break if not found: print(fcounterexample: {n}) return False checked 1 print(fNo counterexample found from 4 to {limit}, checked {checked} numbers.) return True check_goldbach_upto(1000)运行结果No counterexample found from 4 to 1000, checked 499 numbers.看起来很有说服力对吗但这只是验证了 1000 以内的偶数完全没有证明所有偶数都成立。你检查了 10 万个、100 万个、甚至 1 亿个偶数都成立依然不能推出“所有偶数”都成立。这就是有限验证与数学归纳法之间的本质区别。AI 之所以会在这类问题上犯错正是因为它学习了大量“有限样例都成立”的模式然后自信地把结论推广到无穷集合。这种推广从统计意义上可以理解但从数学意义上完全不能接受。形式化证明工具的意义就是把这个“统计自信”替换成“逻辑必然”。但前提是证明确实闭环而且定理陈述没有偏离原命题。5. 用 Lean 写一个真正能被机器检查的证明现在我们亲手用 Lean 写一个可验证的证明。这里假设你是在 Linux、macOS 或 WSL 环境里操作。5.1 安装 Lean 与 elanLean 的版本管理工具叫 elan类似于 Rust 的 rustup。安装命令curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh source $HOME/.elan/env elan default leanprover/lean4:stable不出意外的话安装完成后lean --version应该能输出版本信息。5.2 创建带 mathlib 的项目Lean 社区维护了庞大的数学库 mathlib4。创建一个带 mathlib 的新项目lake new demo math cd demo lake buildlake new demo math会生成一个标准的 Lean 项目包含Demo.lean、lakefile.toml、lean-toolchain等文件。第一次执行lake build需要下载并编译 mathlib 依赖时间会比较长这是正常现象。5.3 写一个最小证明编辑Demo.lean写入以下内容import Mathlib -- 定理自然数加法满足交换律 theorem demo_add_comm (a b : Nat) : a b b a : by omega -- 查看该定理依赖的公理 #print axioms demo_add_comm这段代码定义了一个定理对任意自然数 a、ba b b a。证明使用omega策略它可以自动处理自然数上的线性算术。执行lake build Demo如果一切正常构建不会报错。#print axioms demo_add_comm会输出这个定理依赖的公理列表。你能看到propext、Classical.choice等逻辑公理这表示 Lean 在证明过程中使用了经典逻辑。这通常没有问题但如果你在做构造性数学研究就需要留意。5.4 制造一个“假证明”并识别它再来看一个反面例子。如果你用sorry跳过证明会发生什么theorem fake_theorem : ∀ n : Nat, n 1 n : by intro n sorry #print axioms fake_theorem构建后你能看到警告warning: declaration uses sorry并且#print axioms fake_theorem的结果中会出现一个极其特殊的东西sorryAx。sorryAx是 Lean 内置的一个“公理”用来假装后面的证明成立。任何依赖sorryAx的定理本质上都不是一个完整的证明。检查一个 AI 生成的 Lean 证明是否合格第一件事就是看公理列表里有没有sorryAx。5.5 运行结果如何判断如果构建通过且没有sorry警告证明在形式上闭合。如果#print axioms 定理名只有正常的逻辑公理没有使用非法自定义公理。如果出现sorryAx证明不完整必须打回。如果出现某些自定义的axiom需要单独审查这个公理是否合理。这套判断逻辑和你在npm依赖树里看到一个可疑包时的排查思路是一样的。6. “假证明”最常见的五类模式下面把这几年大模型 形式化证明工具结合时最容易出现的五种“假证明”模式整理出来。它们不一定都出现在这次的争议事件里但你在实际项目中一定会遇到。6.1 用sorry或admit填坑这是最常见、也最容易被忽略的问题。AI 生成证明到一半发现某个子目标暂时证不出来很可能自动使用sorry或admit来跳过。从代码功能上说证明确实编译通过了但从逻辑意义上说这个洞还在。排查方式构建时把warning视为错误。lake build 21 | grep -i sorry如果输出不为空说明存在未闭合证明。6.2 声明额外公理有些 AI 模型为了省事会直接声明一条新的公理然后基于它完成证明。这相当于在代码里引入了一个没有实现的函数然后声称功能完成了。axiom too_good_to_be_true : (∀ n : Nat, n n 1)如果一条公理本身就是你想证明的结论那整个证明就没有意义。排查方法是看#print axioms的输出是否干净。6.3 定理陈述悄悄变弱模型可能把“对所有大于 2 的偶数成立”翻译成了“对所有小于 10000 的偶数成立”或者把“无界”翻译成了“足够大”。Lean 不会质疑这一点因为它只负责检查你给出的、形式化的那行陈述。这类问题也是目前最难自动检测的。没有明确的编译错误也没有非法公理但结论与原命题不匹配。6.4 依赖了不兼容的逻辑假设比如原问题要求构造性证明但 LLM 生成的证明大量使用了反证法、排中律、选择公理。这会让证明在某些数学派别中不被接受。虽然 Lean 会依赖Classical.choice但项目创建者可能根本没意识到这一点。6.5 用运行时计算代替逻辑推导Lean 的native_decide或decide会实际运行代码来判定命题真假。这意味着它把一部分信任转移到了编译器、运行时和硬件上。大多数情况下这是可靠的但对于要求严格逻辑证明的场景它引入了一个不可忽略的信任边界。7. 常见问题与排查思路问题现象可能原因排查方式解决方案构建时出现declaration uses sorry证明未闭合#print axioms 定理名查找sorryAx补全证明禁止sorry进入主线证明能编译但感觉结论太强定理陈述与原命题不符人工对比自然语言证明和形式化陈述建立定理语义审查环节#print axioms中出现自定义 axiom模型引入了额外公理检查该公理是否合理删除自定义公理重写证明Lean 版本不同结果不同环境未锁定查看lean-toolchain文件固定 Lean 和 mathlib 版本AI 生成的证明反复构建失败语法碎片或策略使用错误查看错误行逐步缩减代码让 AI 根据编译错误迭代修正使用native_decide后逻辑上觉得可疑信任了运行时路径检查证明中是否出现运行时关键字替换为纯逻辑推导过程表格里的每一条在实际项目里都可能成为“证明被推翻”的直接原因。8. 最佳实践把 AI 和 Lean 用成一个可信流水线AI 生成数学证明这件事我认为方向是对的但必须把它当成一个需要接口规范、工程审查和日志监控的软件工程问题而不是一个“跑通就算成功”的脚本。8.1 建议的流水线第一步让 AI 先用自然语言写出完整证明思路。这一阶段的目标是理解证明的直觉而不是得到最终答案。第二步让 AI 把自然语言证明转换成 Lean 形式化陈述。这里要特别关注定理陈述与原命题是否一致。第三步用 Lean 写成完整证明并确保没有sorry、没有自定义 axiom。第四步运行lake build把 warning 当作 error 处理。第五步用#print axioms检查证明依赖的公理集合。第六步请有数学背景的人做一次语义审查。这一步不能省略因为 AI 和 Lean 都无法判断“形式化命题”与“自然语言命题”是否真的等价。8.2 项目里要做的加固在项目的lean-toolchain里固定 Lean 版本leanprover/lean4:stable在 CI 里显式检查sorryif lake build 21 | grep -i sorry; then echo FAIL: proof gaps detected exit 1 fi echo PASS: no sorry in proof这只是一个轻量检查。更严格的做法是写一个脚本遍历所有定理的#print axioms输出维护一张允许公理列表任何不在列表里的公理都视为失败。8.3 哪些场景不该用如果项目涉及金融风控、安全协议、密码学证明、核心算法正确性验证一定要记住未经形式化验证的 AI 证明只能作为研究线索不能作为最终依据。即便经过了形式化验证也要通过人工语义审查才能算作真正可信的结论。AI 生成证明确实能大幅降低入门门槛但降低门槛不等于降低标准。把验证流程做好它才是真正提升效率的杠杆跳过验证环节它就是你生产环境里的一颗定时炸弹。9. 结尾这次“AI 证明被打假”的新闻真正有价值的不是看热闹而是让我们重新认识形式化验证工具的作用。Lean 不是一个替你找错误的工具它更像一个极其严格的编译器你给它一个证明它逐行检查但最终证明的是不是你想要的命题它不负责。AI 降低了生成证明的门槛同时也降低了生成“看似证明”的门槛。Lean 这样的证明助手帮助我们把后者大量过滤掉但过滤完剩下的仍然需要人类进行语义层面的审查。建议读者可以在本地装一个 Lean把上面那个最小交换律例子跑一遍再故意用sorry制造一个漏洞亲自看看警告输出和#print axioms里的sorryAx。这种“被内核拒绝”的体验比看任何文章都更能建立对形式化验证的直觉。下一步如果你想深入可以学习 Lean 的归纳证明和策略组合也可以去看看 mathlib4 里真实数学定理的实现方式。把 AI 当作证明的生成器把 Lean 当作审查器把人类当作最终决策者这条链路在可见的未来会是数学与程序世界共同的基础设施。