当发现与证明开始分离：AI 正在重写知识生产的结构

本文来自微信公众号： HavenlonLabs ，作者：Havenlon Labs

过去我们很容易把“找到答案”和“证明答案”理解成同一件事。一个数学家提出一个结论，通常也需要给出证明；一个科学家提出一种理论，也必须解释证据从哪里来；一个工程师给出技术方案，也要说明为什么它能够工作。知识生产因此长期遵循一种很自然的结构：提出答案的人，同时承担相当一部分证明答案的责任。AI正在让这两件事以前所未有的速度分开。

2026年9月，OpenAI公布了一项关于Navier–Stokes方程的研究结果。这个存在性与光滑性问题是Clay Mathematics Institute在2000年提出的Millennium Prize Problems之一。OpenAI表示，其内部AI系统构造了一个有限时间形成奇点的证明，并同时公开了数学论证和Lean形式化证明。OpenAI自己在措辞上依然保持谨慎，最终数学意义上的确认也仍然需要共同体持续审查。几乎在同一时间，Anthropic的Claude将费马大定理已有的人类证明体系形式化为了机器可以检查的Lean代码。Nature报道，这项工作最终形成了约1300万行机器可验证证明，只用了11天，而此前有人估计，如果主要依靠人工完成类似规模的形式化工作，可能需要接近十年。需要强调的是，Claude并没有重新发现费马大定理，Andrew Wiles和Richard Taylor早已完成了证明；真正发生变化的是，AI开始能够把极其复杂的人类数学知识转化成可以被机器逐步检查的形式。

如果只把这两件事理解成“AI数学能力又变强了”，其实会错过其中更值得注意的变化。它们正在暴露一种新的知识生产结构：Discovery≠Verification。发现一个可能成立的东西，与证明它真的成立，正在逐渐成为两种不同的系统能力，而AI的真正影响，也许恰恰不是把这两种能力重新合并，而是把它们彻底拆开。

一、AI首先工业化的，可能不是答案，而是可能性

数学研究从来不只是证明。真正的研究过程往往充满大量并不优雅的工作：寻找模式、尝试特殊情况、改变假设、构造反例、测试边界、搜索已有定理之间的联系，甚至沿着大量最终被证明错误的路线继续走很远。论文最后呈现出来的是一条干净的证明链，但研究过程本身更像是在一个巨大的可能性空间中不断搜索。

人类在这种搜索上有一个天然限制：时间和并行度。一个数学家一天只能认真推进有限数量的思路，一个研究团队能够同时维护的研究路线也有限，因此过去的数学研究天然带有一种“低并发”属性。研究者不仅需要判断一条路线有没有希望，还必须提前决定哪些路线值得投入时间。很多可能性并不是因为它们被证明错误而被放弃，而只是因为没有足够的人力和时间去继续探索。

大规模AI Agent改变的首先就是这个限制。一个Agent可以尝试一种证明策略，另一个Agent可以同时构造反例，另外一批Agent可以搜索相关定理、修改参数、测试边界条件。绝大多数尝试最终可能没有价值，但如果边际搜索成本持续下降，系统就不再需要像人一样谨慎地选择每一条探索路径。它可以允许大量失败，因为失败本身变得便宜。

这意味着AI对科研最早产生巨大影响的地方，未必是“比人类更聪明地完成一次推理”，而可能是把过去昂贵的探索过程变成一种规模化能力。AI最先工业化的，也许不是Truth，而是Hypothesis Generation。它可以以前所未有的速度制造候选答案、候选结构和候选证明，而真正的问题也就随之从“有没有答案”转向了“这么多答案里面，究竟哪些值得相信”。

二、当生成能力暴涨，真正的瓶颈会转向验证

假设过去一个研究团队一年能够提出一百条值得认真检查的研究路线，而未来一组Agent一天就可以生成一万条，那么问题并没有消失，只是从寻找答案转移到了验证答案。以前的问题是“我们能不能找到足够好的答案”，以后越来越可能变成“面对数量巨大的答案，我们怎么知道哪些是真的”。

这是一种非常重要的能力不对称：Generation Capacity>Verification Capacity。生成正在快速变便宜，而验证未必以同样速度变便宜。这个现象其实已经在很多领域出现。AI可以在几秒钟内生成几千行代码，但理解这些代码在复杂生产环境中的真实行为依然很困难；模型可以一次生成几十种商业策略，但判断这些策略背后的假设是否成立仍然需要大量现实信息；Agent可以持续规划下一步动作，但确认每一步的前提、状态和结果是否真的成立，依然属于另一类工作。

过去我们经常把AI的价值理解为“提高生产速度”，但如果生成速度持续超过验证速度，系统最终面对的就不再是生产不足，而是验证债务。软件工程已经让我们见过一次类似的问题：代码写得越快，并不自动意味着系统交付得越快，因为测试、Review、集成、安全检查和生产验证都会逐渐成为新的瓶颈。AI只是把这种不对称从软件生产进一步放大到了知识生产本身。

一个能够产生十万个答案的系统，如果只能可靠验证其中一百个，并不真正拥有十万个可用答案，它拥有的只是十万个候选项。候选答案的数量与可信答案的数量之间，可能会成为AI时代越来越重要的一条边界。

三、Lean的价值，不在于它比AI更聪明

这也是为什么Lean这样的形式化证明系统在这个时间点突然显得重要。Lean并不是一个和大模型竞争“谁更聪明”的AI，它的目标几乎正好相反：把自己限制在一个非常窄的任务里，按照严格定义的逻辑规则检查一个证明过程是否成立。

在人类自然语言数学里，一句话可以省略大量默认知识。“显然可得”“类似可证”“由前式容易推出”，这些表达对专业数学家来说通常没有问题，因为人类会自动补齐背景推理；但对于形式化证明系统来说，这些步骤不能依赖“应该没问题”。定义是什么、使用了哪个定理、输入类型是什么、这一步推导依据什么规则，都必须被明确表达。

于是一个很有意思的结构出现了：一边是能力越来越强、搜索空间越来越大的AI，它负责提出、探索、组合甚至创造；另一边却可能是一个能力非常狭窄、行为极其确定的验证系统，它并不负责产生伟大的数学直觉，只负责回答一个问题——这条证明链在给定规则下到底成立还是不成立。

这其实打破了一种很常见的直觉。我们总容易认为，要监督一个非常聪明的系统，就需要另一个同样聪明甚至更聪明的系统，但很多时候真正有效的结构可能恰恰相反：生成系统需要非常强大，验证系统则需要足够狭窄、确定和严格。前者负责扩大可能性，后者负责压缩可信空间，它们追求的本来就是完全不同的能力。

四、真正重要的变化，是不再要求“发现者本身可信”

这里开始出现一个比数学更大的问题。过去很多系统建立信任的方式，本质上是在判断主体：这个人是不是专家，这家机构是不是权威，这个开发者有没有权限，这个服务是不是经过认证，这个模型是不是经过安全训练。其底层逻辑是，如果能够先确认行动者足够可信，那么它产生的结果就可以获得更高程度的信任。

但数学一直保留着另外一种非常特殊的传统。一个定理是否成立，原则上并不取决于证明它的人是谁。一个毫无名气的研究生如果给出了一条完整而正确的证明，它仍然成立；一个获得过菲尔兹奖的数学家如果证明过程中存在逻辑错误，声望也不会把错误变成正确。数学最终信任的不是主体，而是证明结构。

AI让这种思想突然具有了更广泛的现实意义，因为AI天生就是一种非常奇怪的主体：它可以极其强大，同时又可能犯非常基础的错误；它可以在某些任务上超过绝大多数人类，同时又无法保证下一次推理不会产生一个看似合理但实际上错误的结论。如果继续试图解决“怎样制造一个永远正确的主体”，系统可能会越来越困难；另一条道路则完全不同——允许主体不完美，但要求重要结果必须能够被独立验证。

这是一种结构上的变化。目标不再是消灭错误，而是让错误不能轻易获得“事实”的资格。换句话说，未来真正重要的不是让每一个生成者都足够可信，而是让每一个重要结果都必须经过足够严格的验证。

五、从验证答案，到验证状态变化

数学当然是一个非常特殊的世界，因为数学对象存在于形式系统内部，所以大量问题可以被转换成逻辑规则，并让Lean这样的工具逐步检查。现实世界要复杂得多，但Discovery与Verification分离的思想并不只属于数学。

在软件开发里，程序员或者AI可以写代码，但代码是否能够进入生产环境，还要经过编译、类型检查、测试、CI、Review和部署规则；在数据库里，应用可以提出一次写入，但数据库不会因为调用者“认为应该写进去”就接受它，类型、约束、事务一致性和权限仍然需要成立；在金融市场里，一个交易策略可以提出交易，但最终交易是否能够发生，还受到额度、市场状态、账户状态、风控条件以及清算规则的限制。

这些系统实际上都在做一件相似的事情：把“提出一个动作”与“允许这个动作改变状态”分开。到了AI Agent时代，这种区别会进一步放大，因为Agent与传统软件最大的不同之一，是它开始拥有越来越强的自主生成能力。传统软件的大多数执行路径由程序员提前写下，而Agent可以根据环境动态决定下一步做什么。当执行路径从确定程序逐渐变成动态推理以后，我们就很难再通过穷举所有未来行为证明整个系统永远正确。

这时候，验证对象可能需要发生变化。我们未必能够证明“这个Agent永远不会错”，但我们可以尝试验证“这一次准备发生的状态变化是否满足必要条件”。前者试图证明主体，后者验证一次具体的Transition；前者要求一种近乎绝对的信任，后者则允许主体犯错，只要错误无法自动越过验证结构。

六、可信系统的基本单位，可能正在发生变化

这可能是AI带来的一个非常深的架构变化。传统计算机安全和软件系统非常习惯围绕“主体”建立信任，Identity、Account、Role、Credential、Permission，本质上都在回答“你是谁，以及你拥有什么能力”。但一个主体拥有某种能力，并不意味着它在任何时间、任何状态下做出的任何具体动作都应该成立。

这个问题过去当然已经存在，只是AI让它被进一步放大。当Agent可以连续自主执行几十步、几百步甚至几千步任务时，我们越来越难简单依靠“这个Agent已经认证过”来推导后续所有动作都可信。系统于是可能需要从Trust the Actor逐渐转向Verify the Transition：不只是验证谁在做，还要验证这一次究竟准备改变什么，这个改变是否满足当前状态下的必要条件。

这也是形式化数学真正值得其他AI系统借鉴的地方。Lean最值得关注的并不只是它能够帮助数学家证明定理，而是它体现了一种非常古老却可能重新变得重要的系统哲学：结果是否成立，不应该完全依赖产生结果的主体是否值得信任。

七、未来真正稀缺的，也许不是答案

如果这个趋势继续下去，AI时代有一个非常有意思的经济变化可能会逐渐出现：答案会越来越便宜，代码会越来越便宜，方案会越来越便宜，假设会越来越便宜，甚至研究路线和数学猜想本身也可能越来越便宜，因为产生它们的边际成本正在迅速下降。

但有一种东西不会因此自动变便宜，那就是确认什么值得被接受。当世界拥有一百万个候选答案的时候，真正稀缺的能力就不再只是找到答案，而是建立一套可靠机制，把“一百万个可能”压缩成“几个值得相信的结果”。

从这个角度看，最近数学领域真正值得注意的变化，也许并不是AI又赢下了一项智力竞赛。更重要的事情是，我们第一次如此清楚地看到一种新的分工正在形成：AI可以负责探索巨大的可能性空间，而另一套更加严格、更加确定的系统负责决定其中哪些东西能够获得“成立”的资格。

过去我们总希望制造一个更加聪明、更加可靠、更加接近正确答案的主体；AI可能正在迫使我们接受另一种更加现实的系统观：主体可以非常强大，也可以并不完美，真正成熟的系统并不要求它永远正确，而是要求一个结果不能仅仅因为它看起来足够聪明，就自动获得成为事实、进入系统或者改变状态的资格。

这也许才是“发现”和“证明”开始分离之后，真正值得注意的变化。