AI Agents Formalize Enormous Theorem in Lean, Uncover 40-Year-Old Proof Gap
Axiom Math announced on October 26 that dozens of AI agents formalized the finite simple group classification theorem, known as the Enormous Theorem, into about 43.1 million lines of Lean code in 24 days. The effort, involving 2.05 million formal statements and 715 references, uncovered a proof gap that had existed for nearly 40 years and contributed a new group theory result.
Coverage timeline
机器之心机器之心
编辑｜Neo 100 多位顶尖数学家，耗费数十年，写下 1.5 万页证明。 现在，AI 只用了 24 天，就把这项人类数学史上最庞大的工程之一，变成了 4300 多万行可以由计算机逐步验证的代码。 更惊人的是，AI 在检查这些数学家留下的证明时，还揪出了一个 存在近 40 年的论证漏洞 。 这不是一道奥数题，也不是一篇几十页的数学论文，而是被称为 「巨型定理」（Enormous Theorem） 的有限单群分类定理。 从 20 世纪中叶开始，上百位数学家参与了这场研究。1983 年，数学家 Daniel Gorenstein 宣布分类工作已经完成，但此后人们发现其中仍有未补齐的部分。直到 2004 年，数学家又用 1221 页证明填上了一个关键缺口。 10 月 26 日，AI 数学公司 Axiom Math 宣布，由人类数学家和工程师组织的 数十个 AI Agent，在 24 天内完成了这一巨型定理的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明 ，给出了第一份覆盖整个分类定理的计算机检查证明。 原本分散在 500 多篇论文中的数学推理，如今被组织成一套能够逐步检查的形式系统。更让人意外的是，在这个过程中，Agent 不仅找出历史论文里的错误，还参与构造了一项新的群论结果。 Axiom 公开的有限单群分类定理形式化项目，包含约 4310 万行 Lean 代码、205 万个声明、100 个里程碑，涉及 715 篇参考文献。图源：Axiom Math 官网。 数学界花了数十年，究竟在证明什么？ 理解这项工作的难度，要从「对称性」说起。 一张正方形纸片，旋转 90 度后，形状与原来完全重合；旋转 180 度、270 度也是如此。数学家把这些旋转操作及其组合构成的结构称为「群」。从几何图形到粒子物理，群论提供了一种研究对称性的通用语言。 复杂的有限群，可以在一定意义上分解为更基本的部分。就像整数能分解为质因数，这些不能继续拆分的 「基本粒子」 被称为 有限单群 。 有限单群分类定理 要回答一个看似朴素的问题： 所有这样的基本粒子，到底有哪些？ 最终清单包含素数阶循环群、交错群、16 个无穷系列的李型单群，以及 26 个特殊的「散在单群」。其中最大的 「魔群」（Monster Group） ，拥有约 8×10^53 个元素。光是证明它存在，
Related stories
OpenAI releases 722 AI-generated math manuscripts, claims on quasi-Riemann and Kakeya
OpenAI published 722 mathematical manuscripts produced by an unreleased internal frontier model, grouped into 372 result families across 17 fields, including claims on the quasi-Riemann hypothesis, BSD conjecture, and four-dimensional Kakeya conjecture. The company said most results came from a single prompt to a single AI agent, with average compute per result roughly equivalent to three hours of ChatGPT Pro thinking. Mathematicians described the release as overwhelming, noting it could take years to fully understand, and OpenAI withdrew three papers two days later.
16 reports · 6 sources1334 points · 1520 comments
OpenAI, PerturbAI, Scripps deploy thousands of AI agents to analyze brain-cell CRISPR atlas in 32 minutes
On October 21, 2026, OpenAI, PerturbAI, and Scripps Research announced a study using thousands of AI agents powered by the GPT-Rosalind architecture to analyze a whole-mouse-brain CRISPR perturbation atlas. The distributed workflow completed in 32 minutes, a task estimated to take human researchers months to a year, and aggregated results into a structured reasoning atlas linking gene perturbations to cellular responses and literature.
2 reports · 2 sources159 points · 105 comments
OpenAI claims disproof of Exponential Time Hypothesis, plus math and physics results
OpenAI announced three new discoveries in mathematics, computer science, and physics, including a claimed disproof of the Exponential Time Hypothesis (ETH), a conjecture widely believed for nearly 30 years. The results cover local smoothing for the Euclidean wave equation, the Kakeya conjecture in four dimensions, and a rigorous mathematical existence proof for four-dimensional quantum field theories including quantum chromodynamics. External experts guided the results, and materials were released on GitHub for verification.
5 reports · 5 sources1134 points · 664 comments
Ant Group open-sources Ling-3.1-flash, a 560B-parameter MoE model with 1M context
Ant Group's Ling-3.1-flash, a 560B-parameter mixture-of-experts model with 25B active parameters and a 1M-token context window, was released open-source on October 15. The model targets long-horizon complex task execution, using a hybrid linear attention design with KDA layers and Gated MLA to manage computational costs on long sequences.
News updates every hour. Subscribe in your RSS reader to get new stories automatically.
Subscribe