By Roman Aglaganov
This was an extraordinary week for machine mathematics. Axiom said its AI agents had turned the 15,000-page classification of finite simple groups into 43 million lines of computer-checked proof. OpenAI said its models had proved the Kakeya conjecture in every dimension and disproved a key assumption in computer science, and Anthropic posted its own version of the second result within hours. Each came with a formal proof in Lean, software that checks every logical step.
What a checker checks
Lean is a real advance. If the software accepts a proof, the steps follow from the stated assumptions, and nobody has to trust a tired referee or an AI’s confident prose. That is why these claims deserve to be taken seriously.
But a checker only checks that the proof proves the statement it was given. Whether that statement says what mathematicians mean is a human question. Axiom says so plainly: people must inspect the formal statement and its definitions, while Lean checks the deductions. Its own project showed why that matters. Its agents sometimes proved results under extra assumptions they had not justified, and the team had to throw away tens of thousands of lines.
Access is the bottleneck
Checking now depends on access. Nobody outside Axiom has yet rebuilt its proof, which takes nearly a day of computing. OpenAI has published its maths and computer-science proofs but not its physics materials, which it says the outside physics group chose to hold back. The independent Advisory Group on Mathematics and Artificial Intelligence is right that understanding “should develop in the open, with everyone given the same access.” A claim that only the claimant can inspect is not yet a result.
The reviewers of OpenAI’s computer-science claim set the right tone: they wrote that their involvement “should not be taken as certification of the claim.” That modesty should be the norm.
Understanding is the point
There is a deeper issue. Mathematics is not only a list of true statements; it is a body of understanding. A 43-million-line proof that no person has read may be correct and still teach us little. Axiom deserves credit for publishing a readable paper on the new argument its system found, and for drawing up an errata list with experts. That is the model: let machines do the exhaustive checking, and make sure people can still follow the ideas.
The labs making these claims have the money to help. Funding independent reviews, conferences and the computing needed to rebuild proofs, as OpenAI has started to do, should become standard for every big claim, not a favour.
Disclosure: AI Pulse is written with AI tools, including Claude, which is made by Anthropic.
