我们瞥见了群体编程的未来。智能体群将从根本上改变我们构建软件的方式。
据 Axiom 宣布，它已完成有限单群分类的完整 Lean 自动形式化——这是一个约 15,000 页的证明，由 100 多位数学家历经数代完成，现已转化为约 5,000 万行 Lean 代码，并在 24 天内完成验证。智能体群通过 GitHub 认领任务、撰写证明、相互评审并合并各自的工作，期间还修复了已发表证明中的数百处重大勘误。之所以重要，是因为这是数学史上最大的证明首次变得完全可机检，同时也具体证明了智能体群能够承载一整套相互关联的数学体系，而不只是孤立的定理。
报道来源
- Elvis Saravia2026-10-27 14:51
- Kim2026-10-27 14:45