The Problem With How Mathematicians Work
Mathematical research is one of the most demanding intellectual endeavors in human activity — and, in many ways, one of the least automated. While AI systems have transformed coding, writing, and data analysis, the formal structures of higher mathematics have remained largely outside their reach. Proofs must be verified through rigorous logic; patterns in abstract structures do not yield to the statistical pattern-matching that makes large language models useful for text. A startup called Axiom Math thinks it has found a way to change that, and this week it released a free tool for mathematicians that puts significant pattern-discovery capability on a single laptop.
The tool, called Axplorer, is a democratized version of PatternBoost — an algorithm developed by Francois Charton, a research scientist now at Axiom who previously worked at Meta. In 2024, Charton used PatternBoost running on thousands of supercomputer nodes over three weeks to crack a century-old problem in graph theory called the Turan four-cycles problem. Axplorer can match that result in two and a half hours on a Mac Pro.
What Axplorer Does
The algorithm underlying Axplorer works through an iterative cycle of classical search and neural network learning. It begins by generating a large number of random candidate solutions to a mathematical problem and retaining the best-performing ones. A transformer neural network is then trained on those successful examples to learn what properties characterize a good solution. In the next round, the trained network generates improved candidates that serve as seeds for another classical search phase. The two phases alternate, with each round producing progressively better solutions.
The key insight is that the neural network does not need to understand the mathematics in any deep sense. It needs only to recognize structural patterns in the solutions that have been found so far and use those patterns to guide the generation of better candidates. Over many iterations, this produces solutions that classical search alone would be unlikely to find — particularly in problems with enormous search spaces where random exploration is computationally intractable.
The Turan Problem and What It Reveals
The Turan four-cycles problem asks: given a set of points, how many edges can you draw between them without creating any four-point loops? The problem touches deep structures in combinatorics and graph theory that are relevant to the analysis of real networks — social media graphs, supply chains, and search engine link structures. It had resisted solution for roughly a century before PatternBoost cracked it in 2024.
That PatternBoost required a massive supercomputer was not a barrier for Meta, which operates infrastructure of that scale routinely. But it was a barrier for essentially every mathematician in the world who might want to apply a similar approach to their own open problems. By engineering Axplorer to run on a consumer-grade workstation, Axiom has changed the distribution of access to this class of mathematical AI.
Who Is Behind Axiom Math
The company was founded by Carina Hong, a 24-year-old who dropped out of Stanford after studying at MIT and Oxford. Axiom launched out of stealth in 2024 with $64 million in seed funding at a $300 million valuation, led by B Capital. In addition to Charton, the research team includes Aram Markosyan, an expert in AI safety and fairness.
Hong's vision for the company extends well beyond Axplorer. Finding solutions is not all that mathematicians do — math is exploratory and experimental, she has said. Sometimes insights come from spotting patterns that had not been spotted before, and such discoveries can open up whole new branches of mathematics. Axiom's stated long-term ambition is what it calls mathematical superintelligence — AI that can not only solve known problems but contribute to the discovery of new mathematical structures.
Axplorer Is Free and Available Now
Axiom has released Axplorer as a free tool available to any mathematician who can install it. The decision reflects a deliberate strategy: by distributing the tool widely in the academic community, Axiom can gather feedback, identify which classes of problems the algorithm handles well, and build credibility within a community that tends to be skeptical of commercial AI ventures.
The company's separate product, AxiomProver, which focuses on formal proof generation and verification, has already found solutions to four previously unsolved mathematical problems. The combination of a pattern-discovery tool and a proof verifier represents a complementary pair of capabilities that mirrors the two phases of mathematical research: generating conjectures and then proving them rigorously.
Where Mathematical AI Is Headed
Axiom is entering a field that has seen significant investment and several landmark results. DeepMind's AlphaProof and AlphaGeometry have demonstrated that AI can solve problems at the level of the International Mathematical Olympiad. But competition-style problems, however hard, are a narrow slice of mathematics. The more ambitious goal — contributing to open research in areas like number theory, algebraic topology, or combinatorics — remains largely uncharted.
Axiom's approach, which emphasizes pattern discovery and iterative search rather than end-to-end theorem proving, may be better suited to the exploratory phase of mathematical research than the verification phase. Whether it can generate genuinely novel mathematical insight remains an open question. But the fact that it can now run on a laptop rather than a supercomputer is, by itself, a meaningful step toward answering it.
This article is based on reporting by MIT Technology Review. Read the original article.
