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.
