Thomas Unise
Artificial intelligence has reached a significant milestone in mathematics with Axiom’s AxiomProver system solving multiple unsolved mathematical problems that have stumped experts for years. The breakthrough demonstrates AI’s growing capability to assist and even lead in advanced mathematical research.
The Chen-Gendron Breakthrough
When mathematicians Dawei Chen and Quentin Gendron hit a roadblock in their work on algebraic geometry, they were unable to solve a strange formula from number theory. After ChatGPT failed to help, Chen encountered Ken Ono, a mathematician who had joined AI startup Axiom. The next morning, Axiom’s AxiomProver AI tool presented a complete proof by finding a connection to a 19th-century numerical phenomenon that human mathematicians had overlooked.
How AxiomProver Works
Axiom’s approach combines large language models with a specialized AI system trained to reason through mathematical problems. Unlike standard AI models, AxiomProver can verify proofs using a mathematical language called Lean, allowing it to develop novel solutions rather than merely searching through existing literature.
Multiple Mathematical Breakthroughs
Beyond the Chen-Gendron conjecture, AxiomProver has solved several other significant problems:
- Fel’s Conjecture, concerning syzygies and involving formulas first found in Srinivasa Ramanujan’s notebook over 100 years ago
- A proof involving probabilistic models of “dead ends” in number theory
- A solution that draws on mathematical tools originally developed to solve Fermat’s Last Theorem
Beyond Pure Mathematics
The techniques developed by Axiom could have broader applications, particularly in cybersecurity. The same approaches might help develop software that is provably reliable and trustworthy, creating code more resilient to certain types of attacks.
“Math is really the great test ground and sandbox for reality,” says Carina Hong, Axiom’s CEO. “We do believe that there are a lot of pretty important use cases of high commercial value.”
A New Era for Mathematical Discovery
Ken Ono, who left the University of Virginia to join Axiom, sees this as “a new paradigm for proving theorems.” He hopes AxiomProver will not only assist mathematicians but also reveal something fundamental about how mathematical discoveries are made, potentially making “aha moments” more predictable.
Harvard Business School professor Scott Kominers expressed amazement at the AI’s capabilities: “It’s not just that AxiomProver managed to solve a problem like this fully automated, and instantly verified, which on its own is amazing, but also the elegance and beauty of the math it produced.”
Mathematicians Remain Optimistic
Despite concerns about AI replacing human work, mathematicians like Chen remain optimistic about collaboration with AI tools. “Mathematicians did not forget multiplication tables after the invention of the calculator,” Chen notes. “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.”
GIPHY App Key not set. Please check settings