Exclusive: AI math startup's proofs land in peer-reviewed journals
Add Axios as your preferred source to
see more of our stories on Google.
Illustration: Lindsey Bailey/Axios
A new AI startup tells Axios that proofs created by its algorithms have now been published in several peer-reviewed academic journals.
Why it matters: AI proponents have for years been saying that the technology would lead to scientific breakthroughs and now that appear to be happening.
Driving the news: Axiom Math (no relation to Axios) says proofs produced by its technology — with human-authored articles — have now been accepted by five leading journals.
- They also have more papers under review at journals, eight papers on arXiv and six more in the pipeline.
How it works: Axiom's tool — called AxiomProver — produces full, machine-checkable proofs in a formal language known as Lean.
- Researchers feed it a natural-language problem statement and the model translates the problem into Lean and develops a proof, with a separate checker verifying every step.
- Once the problem is solved, human mathematicians pair the formal proofs with an academic explanation.
- In some cases the system has been given an open research problem and, over roughly 24 hours, has autonomously produced a complete, machine-verified proof, according to Ken Ono, Axiom's founding mathematician.
Yes, but: Large language models, initially mocked for making errors with basic arithmetic, have been making rapid progress in mathematical tasks.
- Last week, OpenAI announced that a forthcoming, general-purpose model solved the planar unit distance problem posed by Paul Erdős in 1946.
What they're saying: Ono characterized OpenAI's discovery as an "exciting development," characterizing Axiom's work as "complementary, but different."
- "We are focused on producing journal mathematics in which human-readable proofs are paired with machine-checkable Lean formalizations and proofs produced by AxiomProver," Ono said.
- "That combination — a conventional mathematical paper together with formal proof certificates —marks an important new step for the field," he added. "To our knowledge, Axiom is the first to bring this model into the journal literature in this explicit way."
The big picture: Axiom said in March that the company raised a $200 million funding round at a $1.6 billion valuation. It's now among a handful of startups trying to produce AI systems focused on being able to solve math problems in ways that are provably true.
- Another is Harmonic, backed by Robinhood founder Vlad Tenev. In January, Nvidia joined a $120 million series C round that valued it at $1.25 billion.
