Axiom 报告称已在 Lean 中形式化有限单群分类定理

发生了什么

Axiom 称，数十个 AI 智能体在 24 天内于 Lean 中形式化了有限单群分类定理，涵盖 500 多篇论文中的约 15,000 页。据 Baoyu 的说法，该系统发现了 John Walter 1986 年证明中的一个漏洞，并采用 Ronald Solomon 1976 年的方法给出了替代证明。Axiom 报告称所有检查均已通过，但尚无独立外部验证的报告；还需要人工审查，以确认形式化陈述与预期定理相符。

接下来读什么

• 今日还有哪些重要变化GPT-6.1 Terra 正式发布

这件事到目前为止

Axiom称，数十个AI智能体在24天内完成了有限单群分类的Lean形式化，且所有检查均已通过。据称，这项形式化涵盖了一项横跨500多篇论文、约15,000页的证明。仍需人工审核，以确认形式化陈述与预期定理相符。 根据Baoyu的说法，Axiom的系统还在John Walter 1986年的证明中发现了一个缺陷，并采用Ronald Solomon 1976年的方法给出了替代证明。