标题里提到的那次“AI证伪百年数学猜想被质疑”的事件在数学圈和程序语言圈都引发了不小的讨论。很多人第一反应是“AI终于能推翻人类智慧结晶了”紧接着又被反转成“形式化证明工具本身出了问题”。如果你只看热搜上的碎片信息很容易得出两个完全错误的结论要么觉得AI数学能力已经强到可以挑战一切要么觉得Lean这类形式化证明工具根本不靠谱。两个判断都太极端了。实际情况是这件事真正值得关注的不是“谁打脸了谁”而是一个我们在工程里天天遇到的老问题工具输出的可信边界到底在哪里。无论是AI生成的证明建议还是形式化验证工具给出的“已验证”结论本质上都是一条流水线上的产物。流水线任何一环出错最终结果都会失真。这次风波只是把数学界、编程语言界和AI圈长期存在的认知差暴露了出来。把它当成一个技术事件去理解其实是在理解“可验证性”这件事本身。1. 先看清这件事在吵什么信息在传播过程中会被不断简化。最开始可能只是一次内部讨论、一个Lean代码库里的细小分歧传到社交平台后就变成了“AI证伪百年猜想”“大学教授破防”这类带有强烈冲突感的叙事。1.1 表面冲突AI被高估还是Lean被高估被议论的所谓“AI证伪”通常是一套完整流程的结果人类研究者提出一个怀疑方向AI模型给出一个可能的反例构造然后由人来检查这个反例是否真的违反了原有猜想。再进一步研究者会把证明过程或反例转换成形式化语言交给Lean等证明助手去机械验证。这里面有一个关键区别AI的输出只是候选Lean的“验证通过”才是最终裁决。如果Lean最后确认构造的反例成立那说明原猜想确实有问题如果Lean无法通过又排查不出代码问题那“反例”就可能只是AI生成的幻觉而不是真正的推翻。这次讨论里最容易被误解的点就在这里。当有人指出Lean证明里有漏洞很多人理解成“Lean验证不靠谱”但实际上更需要追问的是漏洞出现在AI生成的证明代码里还是出现在Lean自身内核的实现里这两个完全不同。1.2 为什么传播中会变成“破防”“破防”这个词放在标题里天然带有情绪张力。但真正参与这个领域的人普遍不会因为一次证明被反驳就情绪失控。做形式化证明的人本来就接受一个前提证明是在限定公理系统和限定规则下进行的超出边界就无效。如果一个AI反例在Lean里通过了机械检查这对研究者来说是值得庆祝的事因为它意味着人类对某个猜想的理解边界被推进了。传播版本里的“破防”更多是围观群众把“哥大教授”这个身份想象成了绝对权威再叠加“被AI打脸”的反转叙事。实际上当一位形式化方法研究者发现证明链条里有漏洞他们通常会先检查是不是自己输入的公理错了、规则选错了、定义和原猜想不一致——这些都属于正常研究工作而不是“破防”。2. Lean强在哪里又弱在哪里要理解这次争议绕不开Lean。它这几年在数学形式化领域声量很大吸引了很多数学家和程序语言研究者参与。2.1 Lean是“证明助手”不是“自动做数学题”很多第一次接触Lean的人会把它想象成一个AI数学解题器输入一个猜想它自动帮你证明。这是很大的误解。Lean更接近一个“证明验证编译器”。它不负责产生灵感而是负责检查你的证明步骤是否在逻辑上严格成立。你可以把它理解成代码的静态检查工具和类型系统的超集你要提供完整的推导步骤它会用内核规则逐步检查每一步是否合法。一旦通过它保证这个证明在它所基于的公理系统内是成立的。这样的设计有一个巨大优点它把“推理”变成了可机械检查的对象。人类看证明会因为知识背景、注意力偏差甚至情绪产生误判而Lean内核只要实现正确就能对证明进行逐符号检验。2.2 漏洞的真正来源但“内核实现正确”是唯一需要担心的吗当然不是。在一个Lean证明工程里出问题的可能性有很多层AI生成证明代码时出错模型可能编造了不存在的引理或者跳过了关键步骤。人类写形式化定义时出错把原数学问题的定义转译成Lean语法时含义可能发生偏移。这相当于把需求文档翻译成代码时产生的bug。选择错误版本的库Lean生态迭代快不同版本的Mathlib接口和引理名称会有差异如果不锁定版本很容易产生意外行为。内核自身实现存在缺陷理论上是可能存在的但概率很低而且一旦被公开验证会产生很大冲击。证明策略被滥用Lean有自动化策略比如omega、linarith它们会尝试自动解决某些子目标。如果目标超出了策略的能力边界策略内部可能静默失败或绕过一个更弱的条件。所以当新闻里说“Lean证明惊现漏洞”时我们要追问这个漏洞属于上面哪一层大多数情况下问题出在形式化定义与原命题不对齐或者AI生成的证明简化了某个条件。真正直达内核的漏洞极少也正因为极少一旦出现就会成为学术圈重大事件。3. 从一次争议提炼出的“AI辅助证明”工作流回到实际工作。如果你对AI和Lean的组合感兴趣希望用它来辅助研究数学习题、验证算法结论或者探索某个猜想更稳妥的做法不是坐等一个完整“AI证明器”而是自己搭建一条“AI出想法、人来审、Lean来验”的流水线。3.1 最小可运行的探索流程我自己在实践里推荐这个顺序也是目前很多研究小组在用的思路先把猜想或命题用自然语言写清楚。不要直接上Lean先用人类语言明确你想证明什么、反例是什么、边界条件是什么。这个阶段可以借助AI做头脑风暴让它生成不同方向的证明思路或者反例构造。把“反例”转成可执行验证脚本。如果AI给了一个反例先不要相信它成立了把它转成Python代码、简单的穷举程序或计算脚本看数值上是否支持结论。这一层过滤非常快能筛掉大量理解错误。再使用Lean做形式化验证。当数值测试已经通过再把命题和证明步骤翻译成Lean。翻译过程中你会被迫定义清楚每一个术语这种“强迫精确”本身就是很大的价值。验证通过后复盘。确认Lean接受了证明再回头对照原命题确认形式化定义没有偏离原始含义。这一步不能省因为“验证通过”不等于“原命题成立”。这个流程的精髓是AI负责“试错”人类负责“判断”Lean负责“最终裁决”。三者各司其职才能避免单一环节的失误被当成整个链条的结论。3.2 为什么会频繁出现“AI幻觉证明”接触过AI辅助证明的人都会发现大模型特别容易生成看起来像模像样、实际完全错误的证明。这不是AI“蠢”而是模型训练目标决定的。大模型在生成文本时优化的是“下一个词的预测概率”不是“逻辑真值”。它非常擅长模仿数学证明的文体却缺乏对每一步前提和结论之间严格因果性的保障。你可以把这种现象类比成一个口才极好但没有经过严格科学训练的人能说出一段听起来无比流畅且很有说服力的论证但细节经不起推敲。因此在AI辅助证明的流程里AI的产出永远只能作为“候选材料”。如果把它当成“答案”直接提交给Lean那等于把错误责任从源头转移到了验证端。Lean不会替你识别“你在证明一个错误命题”。3.3 建议的所有检查步骤我把整个验证链路总结成一个五步排查法这个过程可以复用到很多“AI输出形式化验证”组合场景里检查输入命题是否被正确转述量化关系是否准确是“对所有”还是“存在”这一点极易出错。检查定义原始定义里的每一个条件是否都在Lean的定义中体现有没有因为简化而丢失特殊情况检查引理依赖证明用到的引理是否确实存在是否在同一个版本库中引理名称是否有变动检查策略行为自动化策略是否被误用比如omega只处理线性算术如果输入非线性规则就会失效。检查反例本身如果整个流程最终“证明”了某个反例成立首要怀疑的不是原猜想错了而是你的输入有没有实质偏差。这套步骤看起来朴素但实际项目中大多数“证明漏洞”都是在这里被抓出来的。4. 把“证明被质疑”当工程问题而不是八卦热搜内容会把数学研究包装成智力对抗赛但真实世界里证明被质疑、被复查、被发现漏洞是研究工作的常态。对于做工程的人来说这件事真正值得沉淀的经验是你使用的工具链越强大工具链内部的“信任半径”就要划分得越清晰。4.1 信任半径哪部分可以闭眼信哪部分必须人工盯我把一个AI形式化证明系统里的信任关系分成三层最可信Lean内核本身。它在几十年的研究积累下已经被反复检视但它的保证范围仅限于“在给定定义和公理下证明合法”。条件可信数学库Mathlib及社区维护的引理。多数情况下可用但要关注版本差异和已知弱化。高度怀疑AI生成的证明、人类手工转换的定义、策略的自动推导。这些环节必须有人工审查。这个分层关系可以通用到很多工具场景。比如你用某个静态分析平台扫描代码发现一个漏洞告警同样不能直接把告警当成结论。你要先检查扫描器配置的规则集是否匹配你的技术栈再检查是否产生了误报最后才决定优先级和修复方案。4.2 长期价值在于“把严谨变成基础设施”如果你愿意投入时间搭建AILean的流程真正收获的不是“AI帮我做了数学题”而是“你被迫变得比以往更严谨”。因为形式化验证要求你把每一个隐藏假设都摆到台面上。这种工作方式一旦迁移到日常开发里会有非常明显的长期收益。比如你在写核心算法时可以说“这个算法肯定没问题”但Lean会逼你回答你定义的边界条件是什么索引能越界吗浮点数误差被考虑了吗会不会有特殊输入导致死循环这些原本要靠经验和评审才能发现的问题在形式化过程中会被机械地暴露出来。所以我的判断很明确这件事在新闻里是论战在工程世界里是一次关于流程设计、工具边界和信任半径的普通复盘。如果你愿意可以从安装Lean、跑通第一个证明示例、再让AI辅助你证明一条基础不等式开始。用最小成本感受一下“每一步都能被机械验证”到底是什么体验远比围观“谁破防了”更有收获。