最近 AI 圈和数学圈被一件事同时刷屏有团队宣称用 AI 推翻了一个流传百年的数学猜想随后又被指出证明中存在漏洞连 Lean 这种形式化验证工具也成了争论焦点。事件真假先放一边真正值得开发者关注的问题是当 AI 给出一个“看起来正确”的数学证明时我们凭什么相信它如果换成代码评审等价于同事提交了一版能通过单测、但逻辑有问题的 PR你怎么用工具链守住最后一道防线本文不打算追热点式的复述事件而是把话题拆成一个可操作的技术问题AI 生成数学证明为什么容易翻车Lean 又能帮我们做什么。我会先解释形式化证明与 Lean 的核心概念再带大家在本地搭建 Lean 4 环境用几个完整示例演示“如何验证一个命题”“如何看穿一个带漏洞的证明”最后整理成一套可复用的 AI 证明审查思路。适合正在做 AI 工程、对数学建模或形式化验证感兴趣的开发者阅读零基础也能跟着跑起来。1. 从热点事件说起AI 证明为何会被打假1.1 事件主线与技术争论这次事件的传播路径很典型AI 团队发布成果宣称用大模型“证伪”了某个百年来未被解决的数学猜想消息迅速登上热搜。接着数学和计算机科学社区开始复核很快有人指出推理链条并不完整甚至 Lean 文件里出现了未完成的sorry占位或弱化的定理陈述。最终结论从“AI 攻破猜想”变成了“AI 生成了一个有待验证的证明草稿”。这套剧本其实已经是 AI 辅助科研的“标准剧情”了。大模型擅长生成流畅的推理文本但流畅不等于可靠。尤其是在数学这种对因果链条要求极高的领域一个隐藏假设、一步不成立的推导、一次偷换命题都可能让整个证明从“正确”变成“错误”。对开发者来说更值得关注的是后半段社区如何判定证明有漏洞答案就是形式化验证。把证明写进 Lean让机器逐步检查每一个推理动作一旦跳步或使用未经验证的公理Lean 会直接报错或留下警告。这就像给 AI 证明装了一台“编译器级”的审查器。1.2 为什么“打假”是数学研究的基本功数学史上证明出错并不是新鲜事。很多著名定理在发表多年后才被发现隐藏漏洞原因是传统审稿依赖人的经验而人的注意力终究有限。形式化验证的目标是把“我相信这个证明没问题”升级为“机器逐步确认每一个步骤都合法”。这跟工程里的代码评审很像你写的代码能跑不代表逻辑正确只有通过类型检查、单元测试、人工评审等多层防线才能降低出问题的概率。AI 生成数学证明也一样只不过它把“写代码”变成了“写证明”把“编译器”变成了“Lean”。所以这次事件最大的价值不是嘲讽某个团队而是让更多人意识到AI 可以成为数学研究的加速器但必须配套严格验证。如果你正在做 AI 开发这就是一个绝佳的跨领域实践案例。1.3 本文的实践目标看完这篇文章你会掌握用通俗语言理解 Lean 和形式化证明。在 Linux / macOS 环境安装 Lean 4 和 Lake 项目管理器。用 Lean 定义数学命题并完成证明。识别 AI 生成证明中常见的漏洞类型如sorry、弱化命题、引入额外公理。通过#print axioms检查证明依赖形成一套可复用的 AI 证明审查流程。这些都是可以直接迁移到真实工作的技能。即便你不做数学研究把“如何验证 AI 输出”这套方法论用在代码生成、数据分析、Agent 任务链中也能避开很多隐性坑。2. 核心概念证明助手 Lean 与形式化验证2.1 从“自然语言证明”到“机器可检查证明”传统数学证明以自然语言写成比如“设 n 为偶数则存在整数 k 使 n2k……”。这类证明的优点是阅读门槛低缺点是有大量隐含约定和直觉跳跃。读者如果缺少背景知识很容易忽略某一步其实用到了未被证明的引理。形式化证明则完全不同。它要求把每个定义、每个推理步骤都编码成计算机可以检查的精确规则。你可以把自然语言证明理解为“业务需求文档”把形式化证明理解为“可编译的源代码”。前者讨论的是意图后者必须精确到语法和逻辑关系。Lean 就是一套用于编写和验证形式化证明的系统。它基于依赖类型理论核心思路是把“命题”编码为一种特殊类型把“证明”编码为该类型的一个实例。你声称证明了某个命题等价于你构造出了一个对应类型的实例Lean 的检查器会逐步验证这个实例是否合法。这种设计天然适合数学和程序验证。2.2 Lean 是什么为什么数学社区偏爱它Lean 由微软研究院发起现在是开放社区主导的证明助手项目。目前主流是 Lean 4配套的数学库 Mathlib 收录了大量经过形式化验证的数学定义、定理和证明。规模大到什么程度呢很多现代数学分支都在 Mathlib 中有了基础版本这为在计算机上验证前沿研究提供了扎实地基。与 Coq、Isabelle 等证明助手相比Lean 的语法更接近函数式编程语言学习曲线相对平滑其次Mathlib 社区非常活跃很多当代数学概念已经被形式化方便直接复用第三Lean 的 tactic 机制让证明过程更像“写脚本”你可以一边编写证明脚本一边看 Lean 实时反馈调试体验接近 IDE。不过要注意Lean 不是“自动证明机”。它更像一个“证明裁判”你给出证明步骤它负责检查合法与否。即使有omega、ring、linarith这类自动化策略也主要用于处理局部代数或算术推导整条证明思路仍然需要人来设计。2.3 Lean 与 AI 生成证明的互补关系目前 AI 生成数学证明的主流路径有两种一是直接让大模型输出自然语言证明二是让模型生成 Lean 代码再由 Lean 检查。第二种路径更接近工程实践因为 Lean 的严格性可以有效拦截大模型的幻觉。可以把这套组合理解成“AI 写代码 编译器检查”大模型负责生成候选证明Lean 负责跑编译。如果候选证明有跳步或逻辑错误Lean 会提示错误信息如果模型补上sorry掩盖未完成步骤#print axioms也能查出依赖不干净的证明。这样一来AI 的作用从“定论者”变成了“提出者”最终裁判权始终握在验证系统手里。3. AI 证明中的漏洞从哪里来3.1 大模型的幻觉看起来合理实际上靠不住大模型本质上是根据上下文预测下一个 token它并不具备“逻辑推理”的底层能力。它在训练数据中见过大量数学文本因此学会了“证明该长什么样”开头设变量中间引理最后结论。问题在于这种结构模仿并不保证每一步推导都严格成立。比如模型可能写下“由于 n 是偶数所以 n² 能被 4 整除”这本身没错但下一步它可能写出“因此 n 能被 2 整除且 n/2 也是偶数”这就偷换了前提。人的肉眼很可能被流畅的表达带走Lean 却不会你写成rw [ha]时它要求目标中确实存在可以重写的等号少一个前提都会报错。3.2 逻辑跳跃与隐藏假设数学证明里有两种常见低级错误一种是“少了一步”比如从 A 推到 C 时省略了中间引理 B另一种是“偷偷增加假设”比如证明过程中默认某个变量非负、默认某个函数连续但没有说明条件。自然语言场景下这类错误容易被忽略因为读者会自动补全推导Lean 则要求你显式提供每一步依据隐藏假设在类型层面过不了关。3.3 为什么像 Lean 这样的证明助手能抓住漏洞Lean 的检查器不会因为文本“优雅”就放行。它的每一步战术指令都必须对应到明确的逻辑规则任何一个事实要么是定义展开要么是已有定理要么是当前上下文中的前提否则就无法通过。如果你想用sorry跳过证明Lean 虽然能生成一个“伪证明”但会在文件中留下警告并且#print axioms会显示依赖了不安全的公理。这正是“打假”的核心工具。对 AI 生成证明做验证时我们不是用肉眼去读每一步而是让机器去读然后重点检查三件事定理陈述是否等价于目标问题、证明中是否使用了sorry/admit/axiom、公理依赖是否干净。接下来我们就实际动手做一遍。4. 实战环境本地安装 Lean 4 并创建验证项目4.1 安装 elan 和 Lean 4要在本地运行 Lean首先需要安装 elan。它是一个 Lean 版本管理器类似 Python 生态里的 pyenv负责按项目切换 Lean 工具链。Linux / macOS 可以打开终端执行curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh如果这个地址未来有变化请以 Lean 官方文档为准。安装完成后重新打开终端执行elan --version看到版本信息即说明 elan 已就绪。接下来安装默认工具链elan default stable这条命令会根据stable通道安装当前稳定的 Lean 4 工具链。Windows 用户建议先安装 WSL 2再按 Linux 方式操作可以避开很多原生环境兼容问题。4.2 安装编辑器插件编写 Lean 代码最舒服的方式是 VS Code Lean 4 扩展。在 VS Code 扩展市场搜索leanprover.lean4安装后打开任何.lean文件Lean 语言服务就会自动启动。它的体验类似 IDE 的实时语法检查错误会标红信息面板会给出完整错误列表。也可以使用 Emacs 或 Neovim不过对新手还是推荐 VS Code。4.3 创建第一个 Lake 项目Lean 4 官方推荐使用 Lake 作为项目管理工具类似 Maven 或 npm。在终端执行lake new hello cd hello这会生成一个基础项目典型结构如下hello/ ├── Hello.lean ├── lakefile.toml └── lean-toolchain其中lean-toolchain记录工具链来源lakefile.toml负责项目配置Hello.lean是我们的入口文件。我们重点修改Hello.lean。5. 实战案例用 Lean 验证数学命题5.1 定义“偶数”并证明“偶数之和仍为偶数”为了演示验证流程我选一个非常基础、但足以展示方法论的命题如果两个自然数都是偶数那么它们的和也是偶数。这个命题很简单但它需要你正确展开定义、使用存在量词、完成等式推导和验证复杂定理的流程完全一致。首先在Hello.lean中写入以下代码-- 文件路径hello/Hello.lean def IsEven (n : Nat) : Prop : ∃ k : Nat, n 2 * k theorem even_add_even (m n : Nat) (hm : IsEven m) (hn : IsEven n) : IsEven (m n) : by rcases hm with ⟨a, ha⟩ rcases hn with ⟨b, hb⟩ refine ⟨a b, ?_⟩ rw [ha, hb] rw [Nat.mul_add]这里IsEven表示“n 是偶数”定义方式是“存在一个自然数 k使得 n 2 * k”。rcases用于拆开存在量词取出具体的 a、b 和等式refine告诉 Lean 我们要构造一个存在量词见证后续要证明的等式是m n 2 * (a b)。最后通过rw利用 ha、hb 和Nat.mul_add完成等式变换。5.2 运行验证在项目根目录执行lake build或者直接运行lake env lean Hello.lean如果一切正确Lean 不会输出报错信息说明定理even_add_even的证明通过了形式化验证。你可以在文件末尾临时加一行#check even_add_even再运行就会打印even_add_even : ∀ (m n : Nat), IsEven m → IsEven n → IsEven (m n)这表示even_add_even已经被系统接受为一个类型正确的项。5.3 模拟一个“AI 伪造”的带漏洞证明现在我们来复刻打假现场。假设 AI 输出了一段“证明”但中间用了sorry跳过关键推理。我们在文件中写入theorem fake_even_add_even (m n : Nat) (hm : IsEven m) (hn : IsEven n) : IsEven (m n) : by intro hm hn sorry此时 Lean 不会再保持安静。它会给出警告指出证明使用了sorry并提示这不是一个完整的证明。但问题在于很多工具链仍然允许包含sorry的文件通过编译如果不仔细看警告很容易被蒙混过去。所以真正有效的操作是查看公理依赖。执行#print axioms fake_even_add_even你会看到类似这样的输出sorryAx这意味着该定理依赖了未兑现的sorry公理。严谨的数学验证中这种证明应当被视为无效。AI 生成证明如果经过 Lean 检查但包含sorryAx就等于代码里写了throw new NotImplementedException()却假装功能已完成本质上没有证明任何东西。5.4 编写一个“弱化命题”的陷阱示例另一种翻车方式是偷换命题。比如 AI 想证明更强的结论但最终只证明了一个平凡推论。看下面这个例子theorem weak_version (n : Nat) : IsEven (n n) : by refine ⟨n, ?_⟩ rw [Nat.mul_comm]这个定理是正确的因为n n 2 * n所以nn是偶数。但它只能说明“一个数加它自己是偶数”并不能推导出“任意偶数加偶数仍是偶数”。如果 AI 把weak_version包装成对原猜想的证明那就是典型的“证明不一致”这类问题即使 Lean 能通过也需要人工检查定理陈述是否与目标匹配。这一步非常关键Lean 验证的是“你写的定理”和“证明过程”之间的一致性而不是“你想证明但没写出来的定理”。审查 AI 证明时必须逐字对比定理陈述和原始猜想。6. 如何审查“AI 生成证明”6.1 先检查定理陈述是否与原始猜想一致这是最容易被忽略、但最致命的一步。很多时候 AI 生成的“证明”确实通过了 Lean 验证但验证的是它自己写的一个较弱命题。你要做的是把 Lean 定理翻译回自然语言和原始问题逐字对照看是否存在偷换条件、削弱结论、增加额外前提等行为。例如原始问题可能是“无限多个孪生素数”AI 可能给出“存在无限多个质数”的证明——这在逻辑上完全成立但距离目标差了十万八千里。审查时不能只看证明是否通过还要先问它证的是不是原题6.2 检查是否有 sorry、admit、axiom 残留在 Lean 中sorry和admit是跳过证明的占位命令axiom则是直接声明一个不证自明的公理。真实项目中这三类都应当被禁止出现在最终证明中。审查步骤很简单在 VS Code 中打开 Lean 文件查看是否有黄色或红色警告。搜索关键词sorry、admit、axiom。使用#print axioms 定理名检查公理依赖。如果输出中出现sorryAx、propext、Classical.choice之外的自定义公理就需要格外警惕。propext和Classical.choice是 Lean 的标准公理在常规数学证明中可接受但自定义axiom往往是绕过验证的信号。6.3 用反例和边界条件做压力测试数学证明的漏洞往往藏在边界条件里。拿到一个 AI 生成证明后可以构造一些特殊用例观察结论是否成立。例如检查 n 0、n 1、负数、极大数等边界情况。如果定理声称对所有自然数成立但证明过程中隐式假设了 n 0那么边界测试就能发现问题。在 Lean 中你可以直接写一些example来验证特例example : IsEven 4 : by refine ⟨2, ?_⟩ norm_num如果在边界用例上 Lean 拒绝认证说明定理或证明需要修正。这里的norm_num用于处理数值计算。6.4 交叉验证让 AI 解释并改写证明除了机器检查还可以使用第二个独立模型对同一证明做“解释性改写”。让 AI 把证明的每一步翻译成自然语言并标注每一步用到的引理和前提然后人工核对是否有遗漏。这样做不能替代 Lean 检查但能帮助审查者快速理解证明思路定位可疑步骤。如果把这一步沉淀成流水线大致是大模型生成 Lean 代码。Lean 编译器检查语法和逻辑。#print axioms检查公理依赖。人工对照定理陈述与原始猜想。边界用例测试。第二个 AI 模型改写解释辅助复核。每一层都可能发现新问题。最理想的结果不是“一次通过”而是让所有能自动检查的步骤尽量自动化。7. 常见问题与排查思路问题现象常见原因解决思路unknown identifier IsEven定义没有被解析或文件没有刷新检查定义是否写在引用之前运行lake build刷新项目unsolved goals证明没有覆盖所有目标查看错误面板中剩余目标补全对应 tactic证明中出现sorry但未报错Lean 允许占位符存在搜索sorry用#print axioms检查sorryAx依赖ring或omega策略无法使用未导入 Mathlib在文件头部添加import Mathliblake build下载依赖缓慢Mathlib 文件较大使用预编译的 toolchain配置镜像源或仅构建核心文件定理验证通过但结论可疑定理陈述与原始猜想不一致逐字对照定理陈述检查是否存在弱化命题或额外前提无法使用rcases或rintro当前作用域不存在存在量词先intro引入假设再拆解量词标准库缺少某个数学定义旧版 Lean 或未导入 Mathlib升级至 Lean 4 稳定版确认lakefile.toml引入了 Mathlib遇到报错时建议先看 Lean 信息面板中最顶部的一条错误它往往是后续连锁错误的根源。修完一个再重新编译不要一次修改多处。8. 工程建议AI 辅助数学与科研的正确姿势8.1 把 Lean 当裁判而不是当“证明器”很多初学者误以为 Lean 能自动证明定理实际它只是验证器。写证明时还是要靠人设计思路这在工程上对应的就是把“代码生成工具”和“CI 检查器”分开。AI 负责产生候选方案Lean 负责验收两者各司其职整个流程的可信度才会提高。如果在团队中引入 AI 辅助研究建议把 Lean 验证设为提交门槛。任何 AI 生成的证明只要没有通过 Lean 检查并清理干净公理依赖就不能进入成果发布流程。8.2 建立 AI 输出复核流水线前面在 6.4 节已经给出了流水线雏形。工程实现上可以进一步自动化用脚本批量提取 AI 输出中的 Lean 代码块。调用lake build做编译检查。用正则搜索sorry、admit、axiom等关键词。对每个定理执行#print axioms并解析输出。记录历史结果形成每个 AI 模型的可信度档案。这套流程与代码审查中的静态检查、依赖审计、CI 测试一一对应。如果你已经在做 AI Agent 开发完全可以把 Lean 验证封装成一个工具 Agent专门负责“证明验收”这一环。8.3 学术诚信与安全边界使用 AI 辅助数学研究没有原罪但必须遵守学术诚信底线。AI 生成的结果不能直接宣称“获得证明”或“证伪猜想”必须经过严格的机器验证与同行核查。公开发布时要如实声明哪些部分由 AI 完成、哪些步骤经过了 Lean 验证、验证所用环境版本是什么。从安全角度看也不要轻信来自不可靠来源的 Lean 文件。包含恶意axiom的文件可能在逻辑上“证明”任何结论属于污染公理系统。从外部接收证明文件时务必用#print axioms检查依赖保证只使用标准库和已审定的公理。8.4 从 Lean 到更广阔的形式化验证世界Lean 的价值不止于数学研究。形式化验证方法同样适用于智能合约、协议验证、编译器、分布式系统等领域。如果你在工作中要处理高价值、高风险的代码逻辑抽象出来的方法论是相通的把业务需求编码成精确规范用工具逐步验证实现与规范的一致性。所以即便你的技术栈和 Lean 没有交集也可以把它当作锻炼逻辑严谨性的训练场。当你学会不放过每一条 Lean 报错、不依赖sorry掩盖问题时写业务代码时也会自然多一层警觉。9. 总结与下一步学习路线这一趟下来我们从热点事件出发理解了形式化验证的核心思想动手安装了 Lean 4 和 Lake完成了“偶数之和为偶数”的验证还复刻了用sorry伪造证明、用弱化命题偷换结论的翻车现场。再回顾那次“AI 证伪百年数学猜想被打假”的争议你会发现重点不是某个人或某个团队的对错而是“形式化验证”已经成了科研可信度的重要裁判。下一步如果想继续深入推荐按这个路线走先读 Lean 官方教程掌握intro、apply、rw、rcases、exact等基础 tactic。在 Mathlib 中挑选简单定理进行复现和改写。尝试把某个自然语言证明手动翻译成 Lean 代码体会“跳步”带来的实际报错。结合大模型 API 做一个自动生成 Lean 验证的小工具巩固本文提到的审查流水线。等你能熟练验证十几个初等定理后再回头看 AI 生成的高难度证明你的判断力会比围观热搜时强得多。如果本文对你有帮助可以收藏备用也欢迎在评论区给出你在 Lean 安装或验证过程中遇到的问题我会挑高频问题再写一篇排错笔记。