数十个 Claude 协作 11 天,1300 万行 Lean 代码形式化费马大定理
智东西 · wechat · 2026-09-05
Anthropic 公布:Claude 在 11 天内完成费马大定理首个端到端、可由计算机完整检查的形式化证明,产出约 1300 万行 Lean 代码、30300 个可验证定理(29500 个进入最终证明),代码量达 Lean 核心库 Mathlib 的 5 倍以上,是迄今最大规模的 Lean 证明项目。项目由研究员彭天翼(清华姚班、MIT 博士、哥伦比亚大学商学院助理教授)发起,使用数十个 Claude Agent 并行协作,总消耗约 60 亿输出 Token,模型能力大致相当于 Claude Fable 5.1。
关键在于一套名为 Prove2Me 的协作平台:把证明拆成有向无环图(DAG),不同 Agent 分别认领定义概念、证明引理、向上推进等任务,并可搜索复用已完成结论——多 Agent 直接协作时会互相丢失进度,该平台解决了这个问题。人类仅提供极少高层指导。此前的 Kevin Buzzard 开源形式化项目原计划耗时数年。学界评价:被认为是数学领域最重要的 AI 成果之一,但也有人指出 1300 万行远谈不上简洁,下一步可让 AI 自行压缩证明。
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「公司和人」频道最新
- AI 安全研究者 Sören Mindermann 赴清华任教,共创北京 AI 安全中心 — dhadfieldmenell · 2026-10-21
- Runway 入驻 Claude Marketplace,企业可划拨 Anthropic 预算买视频生成 — runwayml · 2026-10-21
- Pichai:所有人算力都严重短缺,谁都希望计划量翻倍 — firstadopter · 2026-10-21
- GitHub HQ 开放闭源之辩:三场辩论开源方全胜,Percy Liang 谈企业专有知识瓶颈 — stanfordnlp · 2026-10-21
- Meta 将 AI 幻觉责任甩锅用户，被批将加速政府监管 — krishnan · 2026-10-21
- Jacob Posel 用 AI 生成「Harness Your Company」品牌广告概念图 — jacob_posel · 2026-10-21