There’s a difference between an AI that solves known problems faster and an AI that discovers something genuinely new. The first is impressive. The second changes everything.
Axiom’s AxiomProver just crossed that line when it solved Fel’s open conjecture, a real unsolved math problem that’s been sitting in the research literature waiting for someone (or something) to crack it.
Here’s how AxiomProver actually solved it
AxiomProver got three inputs: a document explaining the problem in plain language, a one-line instruction (“State and prove Fel’s conjecture in Lean”), and which proof verification system to use.
First, it read and understood the problem by figuring out what mathematical objects were involved and what needed to be proven.
Next, it translated everything into Lean, a proof language that serves as a strict referee for math. Every single logical move must be justified by basic principles, and the computer verifies that each step is correct. It’s like having a fact-checker that catches every tiny error in your reasoning.
Then came the creative part: AxiomProver chose a proof strategy using exponential generating functions, a technique that converts complicated discrete-math patterns into smoother continuous functions, manipulates them algebraically, and then converts back to prove the original formula holds.
Think of this technique like converting LEGO blocks into Play-Doh, reshaping everything more easily, then converting back to prove the blocks fit together perfectly. Finally, AxiomProver executed the proof step by step in Lean, with every logical move computer-verified. The output: a complete, formally verified proof.
Why this matters beyond math
When AI can discover new mathematical truths autonomously, it’s potentially unlocking breakthroughs in materials science, drug discovery, quantum computing, and any field where unsolved math problems are bottlenecks. In essence, math is the foundation of everything from cryptography securing your bank account to the physics that keeps planes in the air.
The same techniques AxiomProver uses could soon verify that software is trustworthy and immune to hacking. Imagine AI that can mathematically guarantee your medical device won’t malfunction, or your self-driving car’s code won’t fail.
Editor’s note: This content originally ran in the newsletter of our sister publication, The Neuron. To read more from The Neuron, sign up for its newsletter here.