9 月 4 日，Anthropic 对外公布了一项重磅成果：Claude 完成了费马大定理首个完整可计算机校验的形式化证明。消息一出，迅速在科技圈和数学圈刷屏。
不过，很多人误以为 AI 破解了那道困扰数学界 350 年的难题，事实并非如此。费马大定理早在 1995 年就由数学家怀尔斯完成了证明，那份 129 页的论文是写给人类读的，大量推导依赖数学家自身的经验与理解，计算机无法直接核验整条逻辑链。
所谓形式化证明，核心是把整套数学推导翻译成 Lean 机器证明语言，删掉所有“显然可得”这类主观跳过的步骤，让计算机逐行校验每一步逻辑。此前业内预估，这项工作如果靠数学家人力完成，需要耗费数年时间。
本次项目由清华姚班校友彭天翼主导，数十个 Claude 智能体协同工作，仅耗时 11 天，产出约 1300 万行 Lean 代码，证明了三万多条中间定理，最终启用 29500 条完成整套证明。全部代码已经开源，原项目负责人 Kevin Buzzard 完成核验确认有效。
核心亮点并不在于 AI 想出了新解法，而是大规模自动形式化迎来了一个里程碑。未来，这套能力可以用来排查数学论文中隐藏的逻辑漏洞。
但争议同样存在：项目消耗的海量算力，普通科研机构很难复刻；千万行级别的代码，人类几乎不可能通读，AI 生成定义的合理性如何审查，也成了新的行业难题。 | 
发表于 4 天前
|
查看: 5|
回复: 0
