AI 智能体写出 4300 万行代码:Axiom 用智能体形式化验证 CFSG 定理
SucceededMind · x · 2026-10-29
Axiom 正在用智能体对有限单群分类定理(CFSG)做形式化，规模约 4300 万行代码，可能是有史以来最大的开源项目之一。
- CFSG 是数学家数十年积累、约 1.5 万页论证的巨型定理
- 任何一步证明断裂都会导致整体失败，对智能体的长程规划与一致性是极限考验
- 观察智能体逐步拼装这一定理的过程，也再次凸显了背后人类数学成就的震撼
所属事件:Axiom 用 AI 智能体 24 天完成史上最大数学证明的 Lean 形式化(34 条相关)→
「编程与Agent」频道最新
- David Khourshid:Agent 爱用 useState 只因训练数据被它灌满 — DavidKPiano · 2026-10-29
- 用迪士尼动画十二原则打磨 AI 交互,开发者演示丝滑光标动效 — zats · 2026-10-29
- Grok Bot v0.78.1 上线 AI 购物:可代下单、管订阅、自动开免费试用 — mark_k · 2026-10-29
- 生产环境省 LLM 调用的实用架构:编码器+不确定性校准+确定性路由 — camerongreen95 · 2026-10-29
- NPCI 发布 TauIndianBankBench：银行对话 Agent 新基准 — NPCI · 2026-10-29
- 给发帖 Agent 加决策模型：先判断推文是否适合转发到 LinkedIn — marlene_zw · 2026-10-29