Rohan Paul

可验证人工智能的巨大胜利。 形式数学证明开始像软件一样扩展。 @axiommathai 重写了数学中最长的证明，全部 15,000 页，大约 4000 万行 Lean。 在数学家的指导下，大批人工智能代理在 24 天内编写了它。 Axiom 表示，今年年初，让 AxiomProver 编写正确的 10,000 行精益证明花了数周的时间。现在，这群特工在 24 天内正式解决了大约 4,000 倍规模的问题。 目标是有限简单群的分类：大约 15,000 页、500 多篇论文、大约 100 位作者，但没有一个读者读过所有内容。 Axiom 将这一飞跃归功于同时重建三层：模型、线束和基础设施。