自带裁判的科学，最先被AI攻下
三百多年前，费马在一本书的页边写下「我发现了一个绝妙的证明，可惜这里的空白太窄，写不下」。三百多年后，一个语言模型用Lean语言写了十一天，把这块空白填上了。同一个星期，另一间实验室宣布Claude「发现」了一套新的酶系统。科学的城墙不是从正门被攻破的——AI挑的入口，是裁判最铁面无私的那一扇。
十一天，填的是三百年的空白
先看新闻本身。Anthropic宣布完成了首个完整机器验证的费马大定理证明：Claude以Lean语言工作，基本自主地干了十一天。对比一下人类的时间线——1637年费马写下猜想，此后三百多年里数学家们前赴后继，欧拉证了n=3，库默尔用理想数理论扫倒一大片，直到1995年怀尔斯那篇一百多页的论文正式发表，中间还经历过1993年公开宣讲后被发现漏洞、再花一年多与泰勒联手补上的惊魂。人类「证明」它用了三百五十八年，补漏「验证」它用了一年多，评审那份论文用了几个月。机器版本：十一天。
这三个时间的对比，比新闻标题本身有意思得多。数学史上最稀缺的资源从来不是聪明，是确认。怀尔斯的证明问世前，普林斯顿的数学系据说常年收到各地寄来的「证明」，没有一份是真的——因为验证成本太高，数学共同体只能依赖少数几个足够聪明的审稿人的判断力和体力。而Lean把验证变成了机器可以穷尽的事：要么内核接受，要么不接受，没有第三种意见。
所以「十一天」这个数字真正宣告的不是「AI会做数学题」，而是：数学史上最昂贵的那个环节——确认一个证明为真——刚刚被压缩了几个数量级。
为什么是数学先倒下：因为它的裁判是机器
很多人在问「AI什么时候能做出真正的科学发现」，这个问题问错了方向。科学不会被整体攻破，它是被一块一块拿下的，拿下顺序取决于一件事：这个领域的裁判有多干净。
数学是目前唯一一个裁判已经完全机器化的领域。Lean的证明内核是一个极小的可信核心，模型在推导过程中可以胡说八道一万次，最后只看一行判定：类型检查通过，还是不通过。没有审稿人的品味，没有实验污染，没有p值操纵，没有「我觉得这个思路不够优雅」。反馈信号纯净到发指。
这正是Anthropic同一天发布的那篇工程博客的题眼——「一旦Claude能度量某事，它就能让它更快」。可度量的反馈回路是模型的加速器，而数学恰好提供了最纯净的度量：对就是对，错就是错，内核说了算。别的领域拿着嘈杂、缓慢、昂贵的反馈信号，数学把完美信号直接喂到模型嘴边。AI在哪个领域跑得最快，不取决于哪个领域的问题最难，取决于哪个领域的裁判最铁面。
顺着这个逻辑，各领域的「防线强度」其实排得出序：数学有机器裁判，防线最薄；物理有实验，裁判是自然界，慢但诚实；临床医学的裁判是几十年的随访；而有的领域裁判是同行评议——由忙碌、有偏好、有派系的同行组成。哪个裁判最容易被打点、被讨好、被糊弄，哪个领域就最先充斥垃圾，也最后一个真正沦陷。
生命科学的「发现」，发现的是搜索空间
再看另一条新闻。Anthropic的生命科学实验室宣布，Claude做出了一项「实质生物学发现」——一套具有类CRISPR重复结构的新型酶系统，Hacker News上457分、504条评论，热度登顶。
「发现」这个词值得打个引号。从目前披露的细节看，模型做的部分是假设生成与模式识别：在海量基因序列数据里，找出人类注意力扫不到的重复结构。这确实重要——搜索空间太大了，人类直觉的带宽在这个规模面前等于零。但生物学的成本大头从来不在提出假设，而在验证假设：湿实验一轮一轮地做，绝大多数候选死在半路，一轮实验几个月，烧掉的钱以百万计。AI压缩的是「提出候选」这一步，剩下那一千零一步验证，还完好无损地留在实验室里。
市场看得很准。同一周，AI驱动天然产物药物研发公司Enveda完成3.11亿美元融资，用途写得明明白白：推动更多候选药物进入临床试验——翻译过来，就是花钱买验证带宽。资本没有为「AI会想」买单，资本在为「AI想得太多、实验室来不及验」买单。
这也解释了为什么Anthropic能在同一个星期放两颗卫星。发现新酶和证明费马，表面是两个领域，内核是同一句话：把人类最贵的认知环节自动化。在数学那边，自动化连着机器裁判，闭环了；在生物这边，只自动化了前半段，所以后半段还得靠融资养实验室。
比证明更值得盯着的，是那间没人看得见的工作区
同一天还有第三条容易被淹没的新闻：Anthropic的可解释性研究显示，Claude内部存在涌现的「心智工作区」，承载着大量不出现在最终输出里的内部思考。
把它和十一天的证明放在一起，味道就出来了。人类数学家的证明写下来，是写给另一个人看的，每一行都期待被理解。而Lean代码是写给内核看的，人类可以逐行检查每个引理，却不必——也不太会——像读怀尔斯的论文那样通读全局。我们第一次拥有了一种「正确但无人通读」的数学：验证外包给了机器，理解还悬在半空。
那十一天里，模型的「内部」发生了什么？走过多少死胡同？有没有过哪怕类似「灵感」的东西？它的工作区里装着完整的过程，而我们刚刚学会从外面往里看一眼。可解释性研究平时像学院派的自我修养，在这个场景下忽然变成了刚需：当机器开始产出人类不再通读的知识，「理解」这件事就只剩两个候选主体——人类从外面偷看，或者机器从里面自己懂。这场竞争的进度，可能比哪个定理被证明更值得盯。
顺带一句同周的插曲：Claude Code被曝仅在遥测开启时读取开发者的AGENTS.md文件，HN上443分热议，好在问题已修复。一家公司一边让模型替人类发现新酶，一边被抓包多看了一眼用户的配置文件。裁判要干净，球员也得干净——这个行业的信任账户，两边都在记账。
结语：数一数你领域里的裁判
三百多年对十一天，这个对比很容易被读成人类输给了机器。我读出来的完全是另一件事：人类第一次把「证明」和「验证」这两件纠缠了几千年的事干净地拆开，并且把验证那一半，交给了自己亲手造的裁判。这是科学的胜利，只是胜利的账单寄到了数学家名下。
别再问「AI什么时候能做出科学发现」。去数一数你所在领域的验证环节里，还剩多少步骤是必须由人完成的——那几个步骤，就是城墙剩下的厚度。哪天它们也被机器化、被度量化，你的领域就是下一个十一天。