Axiom Math's claim that AI agents turned the longest proof in mathematics into checkable computer code spent two days moving through math Twitter and Hacker News. The project is a complete formalization in the Lean proof assistant of the Classification of Finite Simple Groups (CFSG), a result whose human proof runs to roughly 15,000 pages in more than 500 articles by about 100 mathematicians. Reactions split three ways: relief from mathematicians who long worried the proof could not be fully checked, careful questions about what a machine check actually proves, and doubts about cost and business value.
Axiom's research post is dated October 26. The company's announcement on X went out at 7:34 AM PT on October 27, and the Hacker News thread went up about two hours later. Counts below were checked at about 5:25 AM PT on October 29, 2026: the Axiom post had about 7,060 likes and 3.6 million views, and the Hacker News thread had 239 points and 77 comments. Our news story on the proof covers the math in more depth.
What Axiom says it did
According to the research post, engineers and mathematicians at Axiom directed "swarms of dozens of AI agents" for 24 days, producing about 43.1 million lines of Lean. Lean is a programming language in which definitions, statements and proofs are written precisely enough for a computer to check every step. The first swarm went live on October 2. Agents claimed milestones through GitHub issues, lead agents broke hard arguments into pieces, and other agents searched for existing results or wrote proofs. Axiom says the agents "used a changing mix of models" and does not name them.
The translation turned up problems in the published record. Most were typos, table errors or dropped hypotheses, but Axiom counts "34 noteworthy deviations from the published record that needed to be resolved." The largest involved the Unbalanced Group Theorem, approached through John Walter's 1986 memoir. Axiom's system produced an alternative argument and a new result, "Preservation of simple tops," and the company's mathematicians later found a shorter route that the paper also records. In another case, the agents found a counterexample to a lemma in Aschbacher and Smith's quasithin volumes involving the group SL₂(5). Axiom says it will make the full errata list available in consultation with group theorists; as of October 29, the project's errata page says the list will be published there.
Mathematicians: relief, and some emotion
The most personal post came from @KenOno691, whose X bio lists a professorship at the University of Virginia and a founding mathematician role at Axiom. He wrote: "I was brought to tears on Sunday when the last milestone cleared. My father, a mathematician who passed in Jan, introduced me to the giants of group theory as a kid." The post had about 330 likes. @andrew_v10209, posting as part of the team ("This morning we are releasing"), called it "the largest proof in the history of mathematics" and listed "Over 43 million lines of Lean, 715 papers and books, and 100 substantive fixes to the literature." That post had about 1,880 likes and 100,000 views. The 715 figure matches the "papers and books" count on Axiom's project page, while the research post says the original proof spans "more than 500 articles." The research post counts 34 noteworthy deviations and does not give a figure of 100 fixes.
Outside mathematicians focused on trust. @ObhishekSaha, a math professor at Queen Mary University of London, recalled that as a Caltech PhD student "there were only six people in the world who even roughly understood the whole thing," and called the formalization "a real relief." @tonyyueyu, whose bio lists a Caltech math professorship, collected the old worries ("People who really understand the proof are dying or retiring", "It might not be correct") and said the work turned "this fragile, human-dependent colossal proof into machine-verifiable certainty." Stanford's @jdlichtman posted congratulations.
From the AI side, @kevinweil, formerly OpenAI's chief product officer, wrote "Slowly, then all at once" and said the result is "Now settled beyond a doubt." @TianfuF, a Google DeepMind researcher, wrote that "No one had really verified the whole thing end to end" and asked: "who would sacrifice 10 years of their academic career just to audit someone else's proofs?" The post ends with the hope that AI could settle the ABC conjecture controversy next.
Hacker News: what does a Lean check prove?
One long Hacker News exchange was about trust in the formalization itself. User Panoramix asked how anyone knows the formalization has no errors. User sebzim4500 replied that checking the definitions "isn't that hard" and that the main other assumption is that the Lean kernel is correct, though "the implementations are based on each other so could have a common bug." User adrianN pointed out that "An error in the formalization could also be that you formally prove something different from what you think you proved." pfdietz, who submitted the story, answered that only the statement of the main theorem needs that check. kenferry added that an error would then have to be a bug in Lean, a smaller surface area, with a caveat: they have wondered whether giant proofs give language models an incentive "to find lean bugs to exploit."
Several commenters weighed how big the find was. QuesnayJr wrote they were surprised only one gap turned up, and contubernio replied that "Many many gaps had been found and patched (by humans) already over the last forty years." bamb008 pointed to Axiom's own count of 34 noteworthy deviations. An Axiom staff member, jonath_laurent, joined the thread to say the proof is scattered across more than 500 articles and books, that a swarm of agents was tasked with going through them, and that a hard part was "assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways."
The doubts
Not everyone was sold. vatsachak wrote that "LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct." pred_ asked "What did it cost and how much energy was spent?", a question Axiom's post does not answer. sashank_1509 said they were unsure what Axiom's business model is and that "No one's gonna care" about such a formalization "unless it is very cheap to do." senderista argued that filling known gaps is "the kind of thing the AI companies should be doing, not trying to scoop research in progress."
On X, two small accounts flagged that outside checks are still to come. @subhankarP wrote that "no outside group has independently rebuilt it," and @zshjzls said the real question "is whether the formal statement still means what mathematicians meant."
What it adds up to
The praise is strongest from people who know how fragile the human proof was, and some of it comes from Axiom's own team, so it should be read that way. The open questions are concrete: whether outside teams rebuild and audit the Lean code, what the run cost, and whether the full errata list holds up with group theorists. For AI, the result is narrower than the headline: by Axiom's account, agents proved good at checking and repairing an existing proof at a scale of 43.1 million lines, under human direction. Lean has backed other AI-assisted math this year, such as the 3D Ghys conjecture proof that paired a Shanghai AI Lab model with Lean verification. And Terence Tao has warned that a shift from proof scarcity to proof abundance will test how mathematicians validate understanding.
