A young artificial intelligence startup has used an AI system to crack four previously unsolved mathematical problems, offering a striking glimpse into how machine reasoning is beginning to reshape advanced research.
The breakthrough centers on a company called Axiom, cofounded by mathematician Carina Hong. One of the most notable results involves a conjecture that had resisted proof for years. Mathematicians Dawei Chen and Quentin Gendron originally proposed the idea after running into a mysterious number theory formula they could not justify. Their work remained incomplete, framed as a conjecture rather than a theorem.
Years later, Chen tried unsuccessfully to solve the problem with help from ChatGPT. The turning point came after a chance conversation at a math conference, where Chen mentioned the issue to Ken Ono. Ono had recently joined Axiom after leaving the University of Virginia. By the next morning, Ono returned with a solution generated by Axiom’s AI system, called AxiomProver.
The system did more than fill in missing steps. It identified a connection to a numerical phenomenon studied in the 19th century, something human experts had overlooked. It then constructed and verified a complete proof, which Chen and Ono later posted to the arXiv preprint server. For Chen, the experience was transformative, saying the solution came together naturally once the AI revealed the missing link.
This result is just one of several. Axiom says its system has recently solved multiple open problems across different areas of mathematics. One proof tackles Fel’s Conjecture, a problem involving algebraic structures known as syzygies, with roots tracing back to formulas written by Srinivasa Ramanujan more than a century ago. In that case, AxiomProver developed the entire proof on its own, from start to finish.
Another proof addresses probabilistic dead ends in number theory, while a fourth draws on mathematical tools first developed to solve Fermat’s Last Theorem. None of these problems carry million dollar prizes, but all had resisted expert attention for years.
What sets Axiom’s approach apart is its use of a formal mathematical language called Lean, which allows the AI not only to reason creatively but also to rigorously verify each step. That combination moves the system beyond pattern matching or literature search and into genuinely novel discovery.
Experts say the implications extend beyond pure mathematics. Techniques that generate provably correct reasoning could eventually be applied to software verification and cybersecurity, where correctness and reliability are critical.
For mathematicians, the shift feels profound but not threatening. As Chen put it, calculators did not end the need to understand arithmetic. Instead, AI may become an intelligent partner, accelerating discovery and opening new paths that humans alone might never see.
