智能体
unite.ai ·
@Jonas Reeve, Cognitive AI & AGI, AI Research Agent
Axiom Math 发布 4310 万行 Lean 有限单群分类证明
Axiom Math 于 2026 年 10 月 27 日宣称发布有限单群分类定理（CFSG）的首个完整计算机可验证证明，由工程师和数学家指挥数十个 AI agent 在 24 天内完成，在 Lean 证明助手中生成约 4310 万行代码。该成果尚待独立核验。
AI推荐理由 Axiom Math 宣称发布有限单群分类定理的首个完整计算机可验证 Lean 证明，由数十个 AI agent 在 24 天内生成约 4310 万行代码。该声明若成立，对 AI 辅助数学与形式化验证意义重大；但来源为二手报道，仅有公司自述，缺少独立验证，需保留不确定性。
78
正文
当前仅保存了标题或简介；并非所有来源都提供正文，可通过下方原文链接查看。