最近两个月，AI数学圈的头条有点热闹。
5月，OpenAI宣布其模型反驳了Erdős的单位距离猜想，完整形式化证明连同依赖库约有100万行代码；8月初，其ten-proofs项目又把10个数学与理论计算机科学成果形式化为Lean 4的机器可验证证明证书，据Lean创造者de Moura说，这批问题横跨8个领域，其中就包括Connes刚性猜想的反例。哔哩哔哩知乎
差不多同一时间，Lean和Z3求解器的创造者Leonardo de Moura在播客访谈里给出了一句被广泛传播的话：「我已经不再写测试了。我写性质，然后AI替我证明」。知乎
「已通过Lean形式化验证」正在变成AI成果的信用金标签。但比成果本身更有意思的，是这个夏天连环上演的翻车现场——这个标签本身，正在被圈内激烈争论。
一、双方都拿Lean验证背书，信谁？
8月初，一位叫Nielsen的研究者发文，称OpenAI对Connes刚性猜想的反例不成立：反例不符合猜想条件，核心论证有缺陷。知乎关键在于，这篇「推翻」本身，也用了AI，也拿Lean形式化验证背书。
社区一时有点懵：AI公司用形式化验证背书，否证AI的人也用形式化验证背书，神仙打架，究竟信谁？知乎
答案很快揭晓。OpenAI和Anthropic的研究者先后核对指出，Nielsen的文章存在基本数学错误：立了一个与原文无关的稻草人然后驳倒，还搞混了关键概念；文中一句「显然成立」的步骤，原文其实专门证明了一个辅助猜想才走通。知乎
数学家Shuoxing Zhou同期独立发现了同一反例（过程中也用了GPT-5.6 Sol，但构造思路是自己的），论文8月3日挂上arXiv——殊途同归，从侧面印证OpenAI的结果不是空中楼阁。知乎
有回答说得直白：这些被AI公司宣扬为模型能力的成果背后，人脑的痕迹无处不在，内部反复验证过才敢拿出来。人脑，才是这些成果的终极护栏。知乎
二、「通过验证」不等于「绝对正确」
其实更早的6月就有过一遭：有人宣称证明了P=NP，而且「通过lean 4验证」。知乎
有回答一句话点破：「形式化证出来就对了，是对形式化方法的常见误区。所有形式化方法证明出来的结果，都是相对于作者形式化建模出来的系统而言的。建模和真正想处理的问题之间的偏差，不可忽略」。知乎
类似的追问越来越多。5月知乎有个百万级浏览的对话：「那怎么我们确定这个结果是正确的？」「他通过了形式化验证。」「不是，我不是说那个100多MB的符号推导链条」。知乎8月中旬又有人提问：AI生产的数学证明量级远超人力所及，Lean4是否已经成熟到能验证这些证明？知乎
那么，「通过Lean验证」到底能信多少？答案不是「信」或「不信」的二选一，要拆成三层看。
第一层，证明检查本身，几乎不会错。Lean的证明检查本质是类型检查，承担检查的内核只有约5000行代码，刻意小到任何人可以从头读完。知乎社区还做了多个独立内核互相校验：Mario Carneiro用Lean本身实现了Lean4Lean内核并证明其正确性，还有Rust等语言的独立实现。这一层的可靠性，接近计算器验算。
第二层，形式化的忠实度，才是最容易出问题的地方。机器只保证「这个形式化命题的证明成立」，不保证「这个形式化命题就是你心里那个猜想」。把自然语言猜想翻译成形式语言，本身就是一次解释，解释就可能走样——同一个计算，形式化编码的方式不同，机器验证的对象就不同。Connes事件的核心争议正是「有没有忠实形式化猜想条件」；P=NP事件也一样，证的只是自己搭的那个模型。
第三层，证明出来的东西还得对得上号。圈里有个极端案例要防：验证工具最终输出的命题，不是你想证的定理，而是某个无关的恒真式。知乎所以成熟的外部内核会打印全部已证命题的完整清单和依赖链，方便核对「你证的确实是你要证的」。
一句话总结：机器管推理过程，人管问题陈述。
三、成本曲线是真的塌了
形式化验证今年出圈，不止因为AI数学的热闹，还因为AI把它的成本曲线一脚踹穿了。
几个数字摆在一起看。seL4微内核，AI时代之前的标杆——8700行C代码，验证花了约20人年，每行代码约350美元。知乎
而Lean FRO的Kim Morrison最近用AI把C语言压缩库zlib翻译成Lean并完成验证：大约一周，1100多条定理、约32000行证明代码，证出了压缩引擎最要紧的性质——压缩再解压，一定能恢复原始数据。知乎
反驳Erdős猜想的形式化，从社区发布挑战到完成大约两周；de Moura说，同样的数学基础设施放在过去，要专家手工形式化好几个月。知乎
de Moura的判断是：过去形式化验证的成本约是写程序的10倍，而且最痛苦的不是初始投入，是维护——代码一改，证明就得跟着修。知乎AI恰好最擅长证明开发和证明维护这两件事。
AWS内部已经跑着50万行的Lean项目（一个AI加速器编译器）。知乎华为6月底的形式化方法研讨会，主题干脆就是「AI时代形式化方法：AI Coding可信基础设施」。哔哩哔哩这意味着：形式化验证正在从「关键部件才用得起的奢侈品」，变成AI时代软件工作流的标配。
四、给围观者的实用指南
对普通技术爱好者，这波热闹有两个实用抓手。
第一，下次看到「XX已被形式化验证」的新闻，先问五个问题：是谁做的形式化——模型自己、人类专家，还是人机协作？命题定义建立在什么基础上——Mathlib这样的成熟数学库，还是作者自定义？代码是否公开、可复验——验证通过是一条命令的事，社区复核是第二道防线？社区有没有同行评议，结论如何？形式化命题和自然语言猜想的对应关系，有没有人核对过？五个问题都能答得上来，含金量才高；只有「模型自己说验证过了」的，先当宣传材料放着。
第二，想上手Lean的，门槛比想象中低很多。官网lean-lang.org有函数式编程、定理证明、数学三个方向的免费入门书。知乎还有零基础网页游戏Lean Game Server，更适合完全没接触过的人上手。哔哩哔哩
目前效率最高的学法是「三块屏」：左边Lean代码，右边实时显示剩余目标的info view，底下挂一个AI智能体。知乎陶哲轩现在都是用Claude Code以这种agentic方式做形式化。哔哩哔哩
五、接下来看什么
de Moura给AI划了一条边界：它能找新证明路径、能反驳猜想，但目前没有证据表明它能提出新的数学概念。知乎
而Lean社区里流传的一句话，适合给这波热潮收尾——The point was never "to trust"。知乎形式化的价值从来不是给你一个信仰对象，而是把每一步推理摊开，让它可检查、可反驳。
连陶哲轩这样的头脑，写证明时都会被形式化查出漏掉的特殊情况。知乎
AI越强，「猜」的部分越便宜；人的工作会越发集中在提出对的问题、写对规格说明、核对问题陈述上。这大概是这波AI数学热里，最值得带走的判断。
