Claude 用 11 天自主完成费马大定理首个端到端形式化证明
APPSO · wechat · 2026-09-05
Anthropic 公布新成果：Claude 在几乎自主运行的情况下，用 11 天完成费马大定理的首个端到端计算机验证形式化证明。
- 项目由清华姚班出身、哥伦比亚大学助理教授兼 Anthropic 研究员彭天翼推动，2024 年帝国理工学院 Kevin Buzzard 曾估计同类工作需多年
- 多个 Claude Agent 协同分工，生成约 1300 万行 Lean 代码（超过 Lean 最大数学库 Mathlib 规模 5 倍），构建约 3.03 万个定理，其中 2.95 万个中间定理用于最终证明，共消耗约 60 亿输出 token
- 结果通过 Lean 检查，仅依赖数学基础公理；协作通过开放平台 Prove2Me 管理任务依赖与并行推进
- 背景：怀尔斯 1995 年的人类证明超 100 页，曾因验证漏洞花一年修正；形式化证明让计算机逐步验证逻辑，可能改变未来数学论文「人类解释 + 机器可验证证明」并存的形态
- 文中另提及 Anthropic 随之为 Claude Max 用户重置每周使用额度
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「漫话AGI」频道最新
- Polymarket:OpenAI 年内全面暂停训练的概率仅 7% — Polymarket · 2026-10-21
- Daniel Lemire：AI 量产论文正在戳穿学术界的「教授庞氏骗局」 — lemire · 2026-10-21
- 学者吐槽:大学封杀爬虫下载论文,终身阅读量不足答辩委员会人数 — generativist · 2026-10-21
- 伯克利获 Schmidt Sciences 资助：用 AI 破解抹香鲸与虎鲸语言 — begusgasper · 2026-10-21
- 3Blue1Brown:即使 LLM 能做清晰讲解,我也会继续做视频 — 3blue1brown · 2026-10-21
- Talos 安全研究员:AI agent 攻击尚是吵闹渗透,蜂群静默红队才是真风险 — matthew_d_green · 2026-10-21