Axiom称AI智能体已完成有限单群分类的Lean形式化

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

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。