Claude 证明费马大定理：11天消耗 60 亿Token，成本 30万美元
Anthropic旗下Claude仅用11天便在Lean语言中完成了费马大定理的形式化证明，计算成本约为30万美元——仅相当于一个五年期学术项目经费的三分之一。
这项工作虽然没有产出新的数学发现（该定理早在三十年前就已获证），但它清晰地揭示了AI领域一个关键的经济逻辑：发现变得极其廉价，验证才是真正的成本所在。
OpenAI不久前以约2000美元的成本解决了十个多年悬而未决的数学难题。而Anthropic为验证一个已有三十年历史的定理，却花费了30万美元。两相对照，答案很明确——找到结论几乎不花钱，但要把结论变成无需信任、可被机器严格核查的形式，代价高昂。
这种对“验证”而非“生成”的庞大需求，远超行业此前的预期，正在成为企业部署AI和数据中心建设中被严重低估的变量。
Claude做了什么
帝国理工学院的Kevin Buzzard教授主持着一个由英国EPSRC资助的项目，目标正是用Lean语言将费马大定理形式化。项目为期五年，经费100万英镑。而上周五，Anthropic宣布Claude在11天内完成了同样的工作。Buzzard在博客中写道：
“我拿了100万英镑做五年，Anthropic只用了11天——但我很想知道他们花了多少钱……”
公开信息给出了答案。
Claude生成了1300万行Lean代码，证明了30,300个中间定理，其中29,500个被最终证明采用。整个成果的规模是Mathlib（Lean社区的核心库）的五倍以上。Lean仅凭三条标准公理便验证了全部推理，且定理表述与Mathlib完全一致。整个过程消耗了约60亿个输出Token。
Anthropic使用的模型为内部研究版本，性能大致对标后来发布的Claude Fable 5.1。该模型官方输出定价为每百万Token50美元——60亿输出Token即对应约30万美元。这还只是输出侧的费用，输入与缓存另行计费。当然，公司自用成本低于对外报价，但数量级是清晰的：约等于Buzzard五年经费的三分之一，花在了11天里。#人工智能 #商业 #科技 #美国 #大模型 #数学