Five years ago, mathematicians Dawei Chen and Quentin Gendron were trying to untangle a difficult area of algebraic geometry involving differentials, elements of calculus used to measure distance along curved surfaces. While working on one theorem, they ran into an unexpected roadblock: Their argument depended on a strange formula from number theory, but they were unable to solve or justify it. In the end, Chen and Gendron wrote a paper presenting their idea as a conjecture, rather than a theorem.
Chen recently spent hours prompting ChatGPT in the hopes of getting the AI to come up with a solution to the still unsolved problem, but it wasn’t working. Then, during a reception at a math conference in Washington, DC, last month, Chen ran into Ken Ono, a well-known mathematician who had recently left his job at the University of Virginia to join Axiom, an artificial intelligence startup cofounded by one of his mentees, Carina Hong.
Chen told Ono about the problem, and the following morning, Ono presented him with a proof, courtesy of his startup’s math-solving AI, AxiomProver. “Everything fell into place naturally after that,” says Chen, who worked with Axiom to write up the proof, which has now been posted to arXiv, a public repository for academic papers.
Axiom’s AI tool found a connection between the problem and a numerical phenomenon first studied in the 19th century. It then devised a proof, which it helpfully verified itself. “What AxiomProver found was something that all the humans had missed,” Ono tells WIRED.
The proof is one of several solutions to unsolved math problems that Axiom says its system has come up with in recent weeks. The AI has not yet solved any of the most famous (or lucrative) problems in the field of mathematics, but it has found answers to questions that have stumped experts in different areas for years. The proofs are evidence of AI’s steadily advancing math abilities. In recent months, other mathematicians have reported using AI tools to explore new ideas and solve existing problems.
The techniques being developed by Axiom may prove useful outside the world of advanced math. For example, the same approaches could be used to develop software that is more resilient to certain kinds of cybersecurity attacks. This would involve using AI to verify that code is provably reliable and trustworthy.
“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.”
Axiom’s approach involves combining large language models with a proprietary AI system called AxiomProver that is trained to reason through math problems to reach solutions that are provably correct. In 2024, Google demonstrated a similar idea with a system called AlphaProof. Hong says that AxiomSolver incorporates several significant advances and newer techniques.
Ono says the AI-generated proof for the Chen-Gendron conjecture shows how AI can now meaningfully assist professional mathematicians. “This is a new paradigm for proving theorems,” he says.
Axiom’s system is more than just a regular AI model, in that it is able to verify proofs using a specialized mathematical language called Lean. Rather than just search through the literature, this allows AxiomProver to develop genuinely novel ways of solving problems.
Another one of the new proofs generated by AxiomProver demonstrates how the AI is capable of solving math problems entirely on its own. That proof, which has also been described in a paper posted to arXiv, provides a solution to Fel’s Conjecture, which concerns syzygies, or mathematical expressions where numbers line up in algebra. Remarkably, the conjecture involves formulas first found in the notebook of legendary Indian mathematician Srinivasa Ramanujan more than 100 years ago. In this case AxiomProver did not just fill in a missing piece of the puzzle, it devised the proof from start to finish.