Claude 完成 1300 万行费马大定理 Lean 形式化证明,史上最大机检证明
burny_tech · x · 2026-09-06
Anthropic 官宣:Claude 上个月完成了费马大定理的首个完整形式化证明,总代码量超过 1300 万行 Lean 代码,是迄今最大的 Lean 证明,并顺带机器验证了证明所依赖的 29000 多个其他定理。该项目原被专家认为需要多年才能完成。
- 费马大定理 1995 年由 Andrew Wiles 首次证明,距猜想提出 350 多年;形式化让计算机证明助手可机器验证推理正确性。
- 转发者 nasqret 称主要证明工作由 Kevin Buzzard 带领的学生与博士后团队完成,并指出证明尚未在 Heyting 算术中形式化,他已开始自建 Heyting 算术库作为最后一步。
- 相关仓库 leanprover-community/flt-regular 是证明正则素数情形的 Lean 项目。
所属事件:Claude 11天形式化费马大定理，1300万行Lean代码创纪录(45 条相关)→
「研究」频道最新
- 通用智力指数 GII:用心理测量学从 59 项基准估模型的 g 因子 — wyatt400 · 2026-09-06
- ECCV 2026 将设「几何智能」研讨会，聚焦视觉科学发现 — tolga_birdal · 2026-09-06
- SkillGLoW：存方法不存任务，agent 记忆库缩小 3.6 倍还涨 17.2 分 — rohanpaul_ai · 2026-09-06
- John Langford 组织讨论：为什么需要 world models、要建模什么 — JohnCLangford · 2026-09-06
- PaperLens MCP：不止找代码，还验证论文是否被真正实现 — CraftyScore4348 · 2026-09-06
- AI 或将独力解出 Navier-Stokes 难题,却几乎不给数学留下价值 — NathanpmYoung · 2026-09-06