【清华姚班校友发起，Claude用11天完成费马大定理首个完整的形式化证明】

Kevin Buzzard 收到那封邮件时，正在英国威尔士参加音乐节。他的手机信号很差，短暂连上网络后，他才看到一个陌生人发来的标题：“费马大定理的端到端 Lean 形式化”。这位长期研究数学形式化的帝国理工学院教授，把它当成了又一封不靠谱的邮件。

一周后，整理积压的近千封邮件时，他才知道，对方完成了一项什么工作。随后，他编译了代码，运行检查工具，确认检查通过。

9 月 4 日，Anthropic 公布了这项由其研究员彭天翼（Tianyi Peng）发起的成果：Claude 在人类少量指导下，用 11 天完成费马大定理的完整形式化证明。彭天翼是清华姚班校友，他曾与哥伦比亚大学的合作者开发了数学形式化协作平台 Prove2Me，数十个 Claude 智能体借助该平台协作，生成约 1300 万行 Lean 代码，最终证明使用了约 2.95 万个中间定理。整个过程消耗约 60 亿输出 token。

戳链接查看详情：http://t.cn/AX0ouTxA