AxiomProver: When AI Stops Assisting Mathematicians and Starts Outthinking Them
A new AI system just solved four previously unsolved math problems. But it’s not the solutions that matter—it’s how the AI found them.
The Core Insight
Ken Ono is a famous mathematician who recently left his tenured position at the University of Virginia to join Axiom, an AI startup building systems that can prove mathematical theorems. That alone suggests something significant is happening in AI’s relationship with mathematics.
The proof came when Ono ran into Dawei Chen at a math conference. For five years, Chen and collaborator Quentin Gendron had been stuck on a conjecture involving differentials in algebraic geometry. They’d published their idea as a conjecture rather than a theorem because they couldn’t solve a strange number theory formula it depended on.
Chen had tried prompting ChatGPT for hours without success. But when Ono fed the problem to Axiom’s AxiomProver system, it returned a proof the next morning. The AI found a connection to a 19th-century numerical phenomenon that all the human mathematicians had missed—then generated and verified its own proof.
“What AxiomProver found was something that all the humans had missed,” Ono says.
Why This Matters
AxiomProver represents a significant advance over previous AI math systems for several reasons:
It doesn’t just search—it reasons. Unlike systems that retrieve solutions from existing literature, AxiomProver develops genuinely novel approaches. For the Chen-Gendron conjecture, it synthesized knowledge across different mathematical domains to construct a proof that didn’t exist anywhere in its training data.
It verifies its own work. The system uses Lean, a formal mathematical language, to confirm its proofs are correct. This eliminates the hallucination problem that plagues general-purpose AI systems—mathematical proofs either check or they don’t.
It solves problems end-to-end. The fourth proof Axiom announced, for Fel’s Conjecture about syzygies, was generated entirely by AxiomProver without human guidance. The AI started from the problem statement and produced a complete, verified proof connecting to formulas from Ramanujan’s century-old notebooks.
Harvard Business School professor Scott Kominers, who knows both Fel’s conjecture and Axiom’s technology: “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.”
The Architecture
Axiom combines several approaches:
- Large language models for mathematical intuition and pattern recognition
- Formal proof verification using Lean to ensure correctness
- Proprietary reasoning that enables novel proof construction
This hybrid approach addresses the fundamental tension in AI theorem proving: LLMs are creative but unreliable, while formal systems are rigorous but need to be told what to prove. AxiomProver uses LLMs to generate proof strategies, then validates them formally.
Key Takeaways
AI can now make mathematical discoveries. Not just assist with calculations, but identify non-obvious connections and construct novel proofs that humans missed.
Verification is the key. By integrating formal proof checking, AxiomProver can guarantee its outputs are correct—something no pure LLM can do.
Cross-domain synthesis is emerging. The Chen-Gendron proof required connecting algebraic geometry to 19th-century number theory. AxiomProver made that leap; the human experts didn’t.
Practical applications are coming. The same proof-verification techniques could ensure software is provably correct—a major goal in security and critical systems.
Looking Ahead
Ono says he hopes AxiomProver will reveal something about how mathematical discoveries actually happen: “I’m interested in trying to understand if you can make these aha moments predictable.”
That’s a remarkable statement. If AI can systematize the creative leaps that drive mathematical progress, the implications extend far beyond pure math. Proof verification could become the foundation for:
– Provably secure code resistant to entire classes of vulnerabilities
– Verified AI systems with formal guarantees about their behavior
– Automated research that can explore mathematical spaces systematically
Chen, whose five-year conjecture was solved overnight, remains optimistic: “Mathematicians did not forget multiplication tables after the invention of the calculator. 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.”
Based on: “A New AI Math Startup Just Cracked 4 Previously Unsolved Problems” (WIRED)