Anthropic 上传 Lean 4 费马大定理完整机器验证证明
scaling01 · x · 2026-09-05
Anthropic 在 GitHub 公开仓库 anthropics/fermats-last-theorem，给出费马大定理在 Lean 4 中的完整机器检验证明，基于 Mathlib（Lean 4.33.1、Mathlib v4.33.0 按 commit 锁定）。证明路线为 Frey–Serre–Ribet–Wiles–Taylor-Wiles；PROOF-PATH.md 逐步命名对应的 Lean 定理，html/ 目录可将整个证明作为网页离线浏览。仓库定位为研究工件，不再维护、不接受贡献。
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「模型」频道最新
- 开发者实测:Gemini Argon 分析调试日志优于 Fable 5.1 — ShikharMurty · 2026-10-21
- 用户让 ChatGPT「尖叫」，它陷入无限循环 AAAAHHH 停不下来 — AutomaticScene · 2026-10-21
- 开源新模型 Ornith-1.5-122B 发布:SWE-bench 84.5%,单卡 DGX 可跑 — _akhaliq · 2026-10-21
- Gemini 3.1 Pro 玩「两真一假」：bot 太沉迷账本，秒被识破谎言 — mimi10v3 · 2026-10-21
- 1.3B 开源模型 OXR 登顶三大文档解析榜，百页 101 秒 — aftahi_ai · 2026-10-21
- MiniMax M3.1 Flash 上架 TokenRouter：DeepSWE 73.7%，输出 $0.6/M — MiniMax_AI · 2026-10-21