1000个智能体证完费马大定理 | 你以为AI会做数学了？华尔街笑了，打工人慌了
大家好，我是talk君。
11 月 9 日，一条消息把整个 AI 圈都点着了：1000 个 AI 智能体，没人指挥，只用 30 个小时，就把费马大定理的证明，做成了计算机能逐步核验的形式化证明。
全网都在传同一句话：AI 会做数学了。
但方向错了，而且这里面最有意思的一个点大部分人都忽略了。
先说清楚它到底干了什么。
费马大定理，是数学史上最出名的难题之一，但难归难，数学家怀尔斯早在 1990 年代就证出来了。只不过那份证明，写了上百页，全世界能完整看懂的人，两只手数得过来。
这几十年，一直有人想把这份证明“形式化”，也就是让机器替人把每一行都验一遍，省得靠几个顶尖数学家拿命去校。这事儿极费劲。Anthropic 自己上一回干，靠的是人类研究员在旁边手把手指导，花了 11 天。
这一回，1000 个智能体没人带，30 个小时干完了。证明还缩到了原来的七分之一。所以这次 AI 干的，不是发现什么新定理，它是把那份早就存在的证明，翻译成机器能自动检查的语言。真正变的，从来不是 AI 会不会做数学。
和你有什么关系
你可能觉得，数学证明这种事，离你太远了。费马大定理证没证出来，跟你一个月领多少工资，有什么关系？
关系在于这件事改的，不是数学本身，是一样跟你天天打交道的规矩：一件事到底谁说了算、怎么算数。
往小了说，你今天写代码、写报告、做设计，AI 能不能直接替你交活，取决于一件事：你干的活，别人能不能一眼看出对错。能看出来的，AI 已经可以抢着干了；看不出来的，才轮得到你。
这条线，往下你会看得很清楚。
1
1000个没人指挥的智能体，干的不是推理，是工程
关键不在“30 小时”，在那个“1000 个，没人指挥”。
1000 个智能体，没有一个总司令。它们自己分任务，自己互相检查，谁算错了谁被推翻，最后收敛到一个能通过编译器的证明。你细品一下，这不是一次灵光一闪的推理，这分明是一套工程组织。
我给你打个比方，你可能就懂了。一支 1000 人的施工队，没有项目经理，没有图纸会审，每个人领一块活自己干，干完了互相验收，谁的活儿不合格谁返工。最后大楼封顶，还比人指挥着干快了好几倍。你会怎么评价这件事？你绝不会说“这栋楼特别聪明”，你会说“这套组织方式，了不得”。
AI 这次证费马大定理，就是这么回事。聪明是有的，但真正值钱的，是那套让 1000 个智能体自己组织起来、自己纠错、自己收敛的工程办法。
2
为什么偏偏是数学当了新考卷
顺着这个事，你要问一句：为什么被挑出来当试金石的，是数学？
因为数学有一个别的领域都没有的东西：对错由编译器说了算。
代码跑不跑得通，编译器给你一个干脆的答案。一个证明对不对，机器一步一步查下来，对就是对，错就是错，没有解释空间，也没有人情分。你今天找个关系、说几句好话，都没用，编译器不认。
所以 AI 到底行不行，不用看谁的脸，编译器一句话就判了。
这件事真正的分量，就藏在这里。变的，从来不是 AI 会不会做数学，是“可验证”这件事的价格，第一次变得这么便宜、这么快。过去要花 11 天、还要顶级数学家盯着的事，现在 30 个小时、1000 个机器自己就干完了。
3
它专挑能验真的东西，不是偶然
你顺着“可验证”这条线再往下问一句，就问出点别的了。到这，有意思的事才开始。
Anthropic 这一回拿出来的成绩单，清一色都是能被机器当场验真的：费马大定理、黑洞物理、芯片布线。它为什么专挑这些？
因为这些成果，投资人不用信你的嘴，机器自己会查。你拿一个“模型很聪明、很懂你”的说法去路演，投资人听一半信一半；你拿一个“编译器验过、七分之一长度、30 小时完成”的证明去，投资人没得挑。
这不是我瞎猜。就在发布这条新闻的同一天，答案自己浮出来了。
11 月 10 日，也就是今天，Anthropic 启动了 IPO 路演。路演这两个字，翻译成大白话就是：拿着 PPT 去跟投资人要钱。它的招股书里躺着一个数，算力和基础设施的承诺支出，8954 亿美元。而它刚交出的三季报，营收涨了 1127%，营业上却亏了 5.67 亿美元。
一边是 30 小时证完费马大定理的智力核弹，一边是 8954 亿美元的算力账单。这两件事，就发生在同一家公司、同一个礼拜。
4
最顶级的智力展示，本质是融资路演的开场表演
所以你回头再看那场费马大定理，就全明白了。
AI 行业最顶级的“智力展示”，说穿了，是一场“融资路演的开场表演”。证明费马大定理，不是为了推进数学。是为了告诉华尔街：我们的模型，值得你掏钱。
“可验证”为什么值钱？就值在这：它是最硬的路演门面，硬到没人能还嘴。你别的都可以吹，吹牛、吹情怀、吹未来，投资人能挑刺；唯独“机器验过了”这一条，是一分钱都掺不了水的硬通货。
写在最后
写到这，你可能觉得，这不过是资本圈的一场秀，跟你没什么关系。费马大定理证没证出来，跟我一个月拿多少工资有什么关系？
关系就是：AI最先吃掉的，永远是那些“对错一眼能看出来”的活。
代码跑不跑得通，编译器说了算。证明对不对，Lean说了算。芯片布线合不合格，验证工具说了算。这些领域，AI的产出可以直接交付，因为错了机器会拦下来。
但凡是“对错说不清”的领域（判断一个方案靠不靠谱、审美好不好、一句话该不该说、一个决定敢不敢拍），中间还得有个人。这个人暂时还是你。
问题在于，“可验证”的边界在往外扩。
九月还要人类研究员手把手带的活，十一月1000个智能体自己就干了。今天被编译器验的是费马大定理，明天被验的是你写的那段代码、你搭的那个数据管道、你出的那份报告。Adam Langley用一个周末、每月20美元的订阅，就让LLM自动生成了一个Zstandard解压器的全部正确性证明。这种事在五年前，是20人年的工作量。
我不是在贩卖焦虑。我是在说一个很实际的判断：这十年里，把判断留在不可验证端，把交付往可验证端挪，是你能做的最划算的调整。
费马大定理证没证出来，我不关心。Anthropic能募到多少钱，我也不关心。
我关心的是：当“可验证”变得这么便宜，你站在哪一边。
关注一刻talks。我们不关心Anthropic 能募到多少钱，我只想让你看清一件事：当“可验证”变得这么便宜，还有什么是你要做的？