AI 正在以一种非常奇怪的方式改变科学，而且这种变化既不是很多人想象中的“机器科学家取代人类”，也不是另一派人口中的“高级自动补全终于开始污染学术界”那么简单。真正发生变化的东西，其实是科学发现内部的一种结构，而且这个结构已经存在了几十年，只不过过去它运行得非常慢、非常昂贵、非常局部化，而今天，大语言模型突然让其中一个环节的成本急剧下降，于是整个系统的行为方式开始出现质变。
Donald Knuth，88 岁，《计算机程序设计艺术》的作者，算法分析领域的奠基人，出了名的 AI 怀疑论者，一个几乎代表“传统计算机科学黄金时代”的人物，居然认真阅读了一份 Claude Code 的对话日志，而且不是随便扫两眼，而是逐行检查，因为里面真的出现了让他感到意外的东西。数学家 Filip Stappers 用 Claude Opus 4.6 做了三十一轮组合数学探索，其中第十五轮里出现了一个此前没人明确写下来的结构模式。Knuth 不但认可这个模式，还亲自完成了证明，最后写成论文，并把它命名为 “Claude’s Cycles”。
很多人在这里会立刻滑向两个极端。
第一种叙事非常熟悉：AI 已经成为科学家，人类只是提示词操作员。模型提出了洞见，人类负责阅读结果，科学发现已经自动化。另一种叙事则完全反过来：语言模型根本不理解数学，它只是概率生成器，真正做科学的是研究者，模型只是一个会拼接 token 的随机鹦鹉。
这两种说法听起来都很完整，但问题在于，它们都在试图回答一个错误的问题：“AI 到底有没有在做科学？”真正值得观察的对象其实不是 AI，也不是人，而是两者之间形成的那个循环。
这个循环的结构非常稳定：人类提出问题，模型生成候选答案，某种验证机制过滤这些答案，然后人类决定哪些结果值得继续推进。这个结构在 Knuth 与 Claude 的案例里存在，在陶哲轩与 Lean 的协作里存在，在 AlphaFold 的蛋白质结构预测里存在，在 DeepMind 的 GNoME 材料发现系统里也同样存在。真正完成“发现”的，从来都不是某个单独主体，而是整个 loop。
这件事非常关键，因为它决定了我们应该如何理解 AI 对科学的影响。很多人习惯性地把科学发现想象成一种高度人格化的行为：某个天才突然洞察宇宙真理。但现代科学早就不是这种模式了。真正的大规模科学活动，本质上是一个由提问、生成、筛选、验证、迭代构成的复杂系统，而 AI 恰好在其中最适合“高吞吐量试错”的那个环节上表现出了惊人的效率。
Claude 的案例其实已经很典型。Stappers 做的不是一次“灵感对话”，而是三十一轮系统性探索。模型不断提出候选结构，人类不断筛选和判断，最终 Knuth 对其中幸存下来的结果完成严格证明。这里最重要的角色不是“科学家”或者“AI”，而是 proposer 和 verifier 的分工。模型负责大量生成可能性，人类与数学系统负责验证。
这个 proposer 的概念非常重要，因为它几乎贯穿了所有 AI 科学案例。
陶哲轩最近几年公开讨论过很多次 Lean 与 LLM 的协作。他描述的流程其实极其清晰：大模型提出证明步骤、引理、问题重构方向，而 Lean 的类型检查器负责验证这些步骤是否合法。Lean 不会“觉得差不多”，不会“语言上似乎合理”，它只有接受或者拒绝。形式系统没有模糊地带。于是整个系统形成了一种很有意思的互补：LLM 非常擅长产生看起来可能成立的结构，但它不可靠；Lean 完全不具备创造力，但它可靠得近乎机械。两者组合之后，科学探索开始出现一种新的节奏。
这里真正变化的，不是“AI 学会了数学”，而是 proposer-verifier loop 的运行成本突然下降了几个数量级。
AlphaFold 也是一样。很多媒体喜欢说“AI 解决了蛋白质折叠问题”，但如果仔细看整个流程，你会发现事情根本不是“AI 独立完成科学发现”。AlphaFold 的角色依旧是 proposer：它提出结构候选；真正完成验证的是 X 射线晶体学、冷冻电镜、实验生物学。这些验证机制不是语言模型，它们是物理世界本身。蛋白质到底是不是那样折叠，不由模型决定，而由实验决定。
GNoME 与 A-Lab 的案例甚至更极端。DeepMind 的模型生成了三十八万个候选晶体结构，而 Berkeley 的自动化实验室真的拿这些结构去合成材料。机器人控制真实化学反应、真实高温炉、真实衍射设备，然后检查晶体是否形成。这里的 verifier 已经不是软件，而是自然规律本身。晶体不会因为语言流畅而形成。
如果把这些案例放在一起观察，会发现一个非常稳定的模式：
模型负责提出候选；
独立验证系统负责过滤；
人类负责决定什么值得继续。
这个结构其实比很多人想象得古老得多。
1976 年 Appel 与 Haken 使用计算机证明四色定理时，整个数学界已经经历过一次类似震荡。因为那次证明包含 1482 个需要计算机穷举验证的情况，没有人类能手工检查全部过程。数学家第一次面对一种不再完全可阅读的证明体系。问题是人类提出的，归约过程是人类设计的，而真正完成大规模验证的是机器。
同样的结构后来出现在 Hales 对 Kepler 球堆积猜想的证明中。那份证明复杂到审稿人只能说“99% 相信它正确”。随后 Flyspeck 项目又花了十六年时间，用 HOL Light 完成形式化验证。十六年。这个时间尺度本身就说明一个问题：科学 loop 从来都存在，只是过去 verifier 极其缓慢。
甚至 2020 年的 AI Feynman 也已经体现了类似结构。系统通过符号回归从数据中恢复物理方程，本质上也是 proposer 不断生成数学表达式，再由数学规则进行筛选。
所以 2022 年之后真正变化的东西，其实只有一个：proposer 被通用大模型替换了。
过去每个 proposer 都是专门工程。AlphaFold 是为蛋白质设计的，AI Feynman 是为物理方程设计的，Flyspeck 是为特定数学问题设计的。而现在，一个通用 LLM 可以同时参与组合数学、材料科学、程序搜索、蛋白质结构、形式证明。它未必在任何单一领域都达到专家水平，但它已经足够好，好到 verifier 可以从海量输出里筛出真正有价值的结果。
这个变化看似只是“工具升级”，但实际上它改变了整个科学探索的吞吐量。
因为 proposer 这个角色本来就是整个 loop 中最适合容忍错误的部分。它不需要绝对正确，只需要不断生成“值得验证”的候选即可。真正必须可靠的是 verifier。
这一点在 Galactica 的失败里体现得尤其明显。
Meta 当年发布 Galactica 时，宣传口径几乎是“科学大模型即将改变研究方式”。它读过海量论文，可以生成学术内容、解释概念、提出假设，看起来极其流畅。但它上线三天就被撤回，因为它开始大量生成伪造引用、错误化学结构和虚假事实。
很多人从这里得出的结论是“LLM 不适合科学”。
但更准确的说法其实是：Galactica 缺少 verifier。
它把 proposer 的输出直接暴露给用户，而用户又错误地把 proposer 当成 verifier 使用。整个 loop 没有闭合，于是系统开始稳定地产生“自信的胡说八道”。
这也是为什么 verifier 才是真正重要的部分。
一个弱 proposer 加强 verifier，仍然可以得到可靠科学，只是效率低一点。这其实就是传统科学几百年来的工作模式。相反，一个强 proposer 配弱 verifier，结果一定是灾难。因为 proposer 的任务本来就不是保证正确，它只是负责探索搜索空间。
陶哲轩其实已经非常清楚地意识到了这一点。他对 Lean + LLM 的评价，本质上是在强调两种系统的互补性：LLM 负责创造性，形式系统负责可靠性。单独使用任何一方都不够，但组合之后，整个 loop 的能力突然变得异常强大。
这里最有意思的变化还不只是“生成速度更快”。
更深层的变化是 proposer 开始能够生成 proposer。
像 FunSearch、AlphaEvolve 这样的系统，已经不只是生成候选解，而是在生成搜索策略本身。也就是说，大模型不仅参与问题求解，还开始参与“如何搜索”的设计。这意味着搜索空间本身开始自动演化。
当然，这并不意味着 AI 已经拥有科学主体性。
因为 proposer 并不负责提出问题。
问题依然来自人类。Knuth 决定哪些数学结构重要，陶哲轩决定哪些引理值得推进，材料科学家决定哪些晶体结构有意义。模型不会“关心”某个问题值不值得研究，也不会承担错误发现带来的责任。
所以把 AI 当成“锤子”是不准确的，但把它当成“独立科学家”同样不准确。
更接近现实的描述其实是：AI 正在成为一种新型实验室成员。
它不是 PI，不是作者意义上的主体，但它也不是普通工具。它会提出让专家感到意外的结构，会探索人类来不及穷举的组合空间，会在复杂搜索问题里发现此前没人注意到的路径。它已经不是传统意义上的“执行器”。
而这件事接下来会对整个科学制度产生非常复杂的影响。
因为科学机构真正衡量的东西，从来不是“发现”本身，而是论文。
问题在于，论文数量与真正科学突破之间，其实早就脱钩了。
Nature 2023 年一项研究已经指出，自 1945 年以来，真正具有“颠覆性”的研究比例一直在下降，而论文数量却持续爆炸。大量论文只是微小增量、重复验证、方法迁移。AI proposer 的出现，只会进一步放大这种趋势。
因为生成候选结果的成本突然降低了。
如果一个模型一天能生成上千个“看起来像论文”的候选结果，而 peer review 本身又是一个极其脆弱、缓慢、可操纵的 verifier，那么整个学术系统会立刻面临前所未有的噪声洪水。
所以 AI 对科学最大的挑战，其实不是 proposer，而是 verifier。
今天几乎所有资本都在疯狂投入 proposer：更大的模型、更低的推理成本、更快的生成速度。但 verifier 的建设严重滞后。形式化验证工具依然难用，实验复现缺乏激励，自动化实验室成本高昂，学术审稿系统仍然停留在“论文生成很昂贵”的旧时代。
可未来真正稀缺的人，恰恰是那些能够设计 verifier 的研究者。
因为当 proposer 极度廉价之后，真正有价值的能力会向上游转移：提出正确问题，以及构建可靠验证机制。
未来最重要的科学家，很可能不是“最会写论文的人”，而是那些能够定义“什么叫正确答案”的人。
所以如果今天看到某个“AI 科学突破”，其实只需要问一个问题：
它的 verifier 是什么？是谁构建的？
如果 verifier 是 Lean、实验物理、晶体衍射、严格复现实验，那么结果值得认真看待。因为 proposer 是否可靠已经不再重要，垃圾会被 verifier 清除。
但如果 verifier 也是 GPT-4，本质上只是“让另一个模型判断第一个模型是否合理”，那其实仍然是 Galactica，只不过包装得更复杂一点。
真正决定科学质量的，从来不是 proposer，而是 verifier。AI 改变的不是这个事实，而是它第一次把 proposer 的能力推到了一个极端，以至于整个科学体系不得不重新意识到：验证，才是整个 loop 里真正昂贵、真正关键、真正不可替代的部分。