Axiom, an artificial intelligence startup, says its math system has recently produced proofs for four problems that had remained unsolved. The claims do not place AI at the summit of mathematics, but they do show a tool moving from classroom-style exercises toward problems that working experts had not resolved.
The central system is AxiomProver, a proprietary AI tool built to reason through mathematical questions and check whether its answers are provably correct. Its recent results include work in algebraic geometry, number theory, syzygies, and other areas where proof is the standard that matters.
A conjecture that started with a roadblock
Five years ago, mathematicians Dawei Chen and Quentin Gendron were studying a difficult problem in algebraic geometry involving differentials, which are elements of calculus used to measure distance along curved surfaces. Their work ran into a complication: one part of their argument depended on an unusual formula from number theory, and they could not solve or justify it.
Because that piece was missing, Chen and Gendron presented their idea as a conjecture rather than a theorem. The difference matters. A conjecture can point to a true mathematical pattern, but it remains unproved until someone supplies a valid argument.
Chen later tried to push the problem forward by prompting ChatGPT for hours. That effort did not produce the solution. The turn came during a reception at a math conference in Washington, DC, last month, where Chen spoke with Ken Ono, a well-known mathematician who had recently left the University of Virginia to join Axiom.
Axiom was cofounded by Carina Hong, one of Ono’s mentees. After hearing about the problem, Ono returned the next morning with a proof generated by AxiomProver. Chen then worked with Axiom to write it up, and the proof has been posted to arXiv, a public repository for academic papers.
“Everything fell into place naturally after that,” says Chen.
What AxiomProver appears to be doing differently
The system did not simply retrieve an existing answer. According to the source account, AxiomProver found a link between the Chen-Gendron problem and a numerical phenomenon first studied in the 19th century. It then produced a proof and verified it.
“What AxiomProver found was something that all the humans had missed,” Ono tells WIRED.
Axiom’s method combines large language models with its own math-reasoning system. The goal is not just to generate plausible mathematical text, but to reach answers that can be checked as correct. AxiomProver uses Lean, a specialized mathematical language, to verify proofs.
That verification layer is important because math is unforgiving. A proof must hold up step by step. A fluent explanation is not enough, and a model that sounds confident can still be wrong. By using Lean, AxiomProver can test whether the structure of a proof satisfies formal requirements.
The article compares the broad idea with Google’s AlphaProof, a system demonstrated in 2024. Hong says that AxiomSolver includes several significant advances and newer techniques.
Four problems, not one
The Chen-Gendron conjecture is only one of the recent results Axiom is pointing to. The company says its system has generated several solutions in recent weeks, including answers to questions that had challenged experts in different areas for years.
One proof concerns Fel’s Conjecture, which involves syzygies, or mathematical expressions where numbers line up in algebra. That work has also been described in a paper posted to arXiv. The conjecture is connected to formulas first found in the notebook of Srinivasa Ramanujan more than 100 years ago.
In that case, AxiomProver did more than complete a missing part of a human argument. It devised the proof from start to finish.
Scott Kominers, a professor at Harvard Business School who is familiar with Fel’s conjecture and Axiom’s technology, described the result as striking. He pointed not only to the system’s ability to solve the problem in a fully automated and instantly verified way, but also to the mathematical quality of the proof it produced.
The third proof generated by Axiom’s AI involves a probabilistic model of so-called “dead ends” in number theory. The fourth uses mathematical tools that were originally developed to attack and ultimately solve Fermat’s Last Theorem, one of mathematics’ most famous challenges.
Why the result matters beyond math
The proofs do not mean AI has solved the most famous or most lucrative problems in mathematics. The source article is clear on that point. Still, the results suggest that AI math tools are becoming useful in the professional research process, not only in demonstrations or training benchmarks.
Ono sees the Chen-Gendron proof as evidence that AI can now assist mathematicians in a meaningful way.
“This is a new paradigm for proving theorems,” he says.
The same techniques may also have uses outside advanced mathematics. Axiom’s approach could help develop software that is more resilient to certain kinds of cybersecurity attacks. The idea would be to use AI to verify that code is provably reliable and trustworthy.
Hong frames mathematics as a proving ground for broader applications.
“Math is really the great test ground and sandbox for reality,” says Hong, Axiom’s CEO. “We do believe that there are a lot of pretty important use cases of high commercial value.”
From tool to partner
The broader question is not whether mathematicians disappear from the process. In the examples described, humans still define problems, judge significance, write up results, and interpret what the proof means. But AxiomProver appears to be taking on a more active role in discovery than ordinary software tools.
Ono says he hopes systems like AxiomProver can help reveal how mathematical discoveries happen. He is especially interested in whether the sudden moments of insight that drive research can become more predictable.
“I’m interested in trying to understand if you can make these aha moments predictable,” he says. “And I’m learning a lot about how I proved some of my own theorems.”
Chen, after seeing his own conjecture solved with Axiom’s help, is also optimistic. He compares AI to earlier tools that changed mathematical work without replacing mathematical understanding.
“Mathematicians did not forget multiplication tables after the invention of the calculator,” Chen says. “I believe AI will serve as a novel intelligent tool—or perhaps an ‘intelligent partner’ is more apt—opening up richer and broader horizons for mathematical research.”