Axiom Math says proofs created by its algorithms have now been published in several peer-reviewed academic journals. The company says proofs produced by its technology, combined with human-authored articles, have now been accepted by five leading journals. It also says it has more papers under review at journals, eight papers on arXiv and six more in the pipeline.
The company’s tool, AxiomProver, produces full, machine-checkable proofs in a formal language known as Lean. Researchers provide a natural-language problem statement, and the model translates the problem into Lean and develops a proof, with a separate checker verifying every step. After 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, autonomously produced a complete, machine-verified proof, according to founding mathematician Ken Ono.
The advance comes as large language models have been improving on mathematical tasks after early criticism over basic arithmetic errors. Last week, OpenAI announced that a forthcoming, general-purpose model solved the planar unit distance problem posed by Paul Erdős in 1946. Ono called that result an exciting development and described Axiom’s work as complementary but different, with a focus on journal mathematics that combines human-readable papers with machine-checkable Lean formalizations and proof certificates.
Axiom said in March that the company raised a ? million funding round at a ?.6 billion valuation. The startup is part of a small group of companies building Artificial Intelligence systems designed to solve math problems in ways that are provably true. Another is Harmonic, backed by Robinhood founder Vlad Tenev. In January, Nvidia joined a ? million Series C round that valued it at ?.45 billion.
