费马定理被机器验证，创业者该看哪里

上周三晚上九点多，我在办公室过现金流表，产品同事甩来一条消息：Anthropic 说 Claude 基本自主运行 11 天，完成了费马大定理首个端到端、经过计算机检查的形式化证明。我看了两遍，没先聊数学，先问：这个能不能搬到合同审核里。

这个方向值得关注，但落地是关键。

费马大定理离创业公司很远。1995 年怀尔斯用 129 页论文解决，困扰数学界三个半世纪。这次也不是 AI 重新发明定理，而是把已有证明翻译成 Lean 能逐步验证的代码。据说整个过程生成了大约 1300 万行代码。重点不是 AI 会做数学，而是它把一个超长、超碎、需要严格检查的工程活，压缩到了 11 天。

这很像我们最近用 Claude 做的事。我大概用了一个月，主要不是聊天，是拿它做旧代码迁移、文档转 schema、测试用例补齐。模型自己跑 11 天这种事，我这边没这么夸张，但长任务确实出现了：以前要拆成几十个小需求，现在可以给一个目标，让它在边界里反复试。问题是，长任务一旦失控，烧的是 GPU、人力和客户信任。

所以我不想把它写成通用 AI 又突破了。更实际的对比是两条路线。

路线	它解决什么	创业公司怎么看
模型端到端形式化	把已有复杂材料转成机器可验证结构	适合有明确验收标准的长任务，比如测试、迁移、条款抽取
人工加规则引擎	把专家经验固化成稳定系统	适合高风险、低容错、需要追责的场景，但启动慢、维护重

第一条路线的漂亮之处，是它把理解材料和验证材料接上了。人写证明，机器检查；人写业务规则，机器执行。第二条路线的稳，在于每一步都有人签字，出错知道找谁。创业公司不能只看第一条路线的快，也不能死守第二条路线的慢。真正要算的是毛利、回款和错误成本。

我之前写过一篇，说先搭验证闭环，再买 AI 算力。这次形式化之所以能成立，关键不是模型多能生成，而是 Lean 给了硬检查器。没有检查器，1300 万行代码只是噪声。企业里也一样：AI 能生成一堆东西，但客户说不对，我们拿什么证明它对。单元测试、schema、编译器、审计日志、回滚记录，才是 AI 产品的地基。

很多团队做 Agent，容易把 demo 当交付。实际落地会遇到边界情况、权限、脏数据、责任归属。我这边测下来，处理结构化数据确实省事，前提是数据本身规整。数据脏的话，前面清洗的功夫一分都省不掉。

从商业模式看，更值钱的可能是行业验证套件。比如合同抽取，不只是生成条款，还要能标注来源、输出差异表、让人复核。谁能把 AI 生成变成可审计流程，谁就有定价权。

我创业第三年，带 30 人团队，不太建议一上来就 all in 自主 Agent。先找内部任务：输入输出明确；结果能被机器部分检查；失败可回滚；省的是重复人力，而不是替代关键判断。比如旧系统迁移，让模型列依赖、生成补丁、跑测试。合同审核让模型抽字段，规则引擎查冲突，人只看异常。

成本也要算。11 天背后是算力、调度和模型调用。我们之前用云端 GPU 四周，发现白天在线任务、晚上批处理成本差很多。自主长任务最好设 token 预算、时间预算、最大重试次数。超过阈值就停下来交给人。

团队至少需要三种人：懂业务、懂验证工程、懂客户。创业公司常常业务靠老板讲，工程靠临时脚本撑，这种团队接不住长任务 AI。

看这条新闻，我会把它当成工程信号，不是数学奇迹。AI 的边界在变，变的是它能连续处理复杂材料的时间长度。能不能赚钱，看的不是它会不会生成，而是我们有没有办法让结果可检查、可追责、可交付。

给一个行动建议。明天回公司，别先开大模型战略会。选一个内部任务，写出验收条件，先让 AI 跑小样本。如果它生成的东西能被机器判断对错，再谈自动化；如果判断不了，先别买算力。先把验证闭环搭起来，再谈 Agent。