The way we do mathematics is changing. Informal large language models can be a good tool to streamline literature searches, explain complex concepts, and even sharpen one’s mathematical arguments. At the same time, we at Axiom are building a prover system empowered by reinforcement learning and formal verification that automates large portions of proofs, handling technical lemmas that once took hours of a mathematician's time. This synergy marks a true and powerful revolution in the way mathematical discovery is done.

Yet it’s still day zero. “Math AGI Achieved” headlines overlook one fact: we've been here before. When symbolic notation emerged in the 17th century, it revolutionized mathematical thinking. The arrival of computers turned once-promising broad research areas – such as calculating precise approximations of pi or solving specialized systems by hand – into niche pursuits in between math and computer science. Stunningly, the four-color theorem and Kepler's conjecture became solvable because we could verify millions of cases. Every time, naysayers claimed the subject would become obsolete. Every time, they were wrong.

Will chatbots "doom" mathematics? Are we headed toward a future where machines turn us into passive spectators of LLMs’ magic, amateur solvers of AI brainteasers, or data labellers? Some advocates of large language models seem to believe so.

At Axiom, we see a richer future, demanding a diverse approach that’s not one-size-fits-all. Our prover team builds rigorous verification systems. Today, we're introducing our discovery branch: a new kind of science that generates novel mathematical objects, and connects them back to proofs.

Every text on the history of science clearly illustrates Thomas Kuhn's profound influence. In 1962, he distinguished between "normal science" – the steady, incremental progress built on previous knowledge – and major paradigm shifts that completely change the rules. Mathematics thrives on these revolutionary changes.

Consider this: 16th-century mathematicians were able to articulate formulas for cubic and quartic roots, showcasing remarkable symmetry. Then Galois appeared and decisively demonstrated that such extensions are impossible for higher degrees. But he didn't just show a negative result. He introduced transformations that kept the invariance of the equation roots – planting the seeds of group theory. More recently, Grothendieck didn't just contribute to algebraic geometry – he revolutionized it entirely with schemes, fundamentally transforming the field.

These works are more than mere refinements. They opened new universes of mathematics.

Mathematical objects are purely abstract, with no physical reason to favor one over another. Despite this, mathematicians have a remarkable talent for choosing the right abstractions – those that are both beautiful and occasionally useful. Eugene Wigner called it "the unreasonable effectiveness of mathematics," where these abstract toys keep showing up as the exact tools physics requires to describe reality.

How does this magic happen? Through discovery. Not literature searching. Discovery means conjuring genuinely new mathematical objects and exploring their potential.

Large language models are pattern synthesis machines. They've read everything, and they're excellent at remixing existing knowledge. Need to adapt a proof technique from topology to number theory? They'll suggest three methods. Want a summary of current research on elliptic curves? They'll write you a survey paper.

But here's their Achilles' heel: they're trained to synthesize, not to leap. Their extensive pre-training on existing text and their autoregressive generation mode bias them toward interpolating within the known distribution. They're the ultimate "normal science" accelerators. Paradigm shifts require out-of-distribution thinking – exactly what transformers struggle with when they're pre-trained on everything humanity has written.

Provers, an important part of our system, can sometimes face the opposite challenge. As AI mathematicians, their personalities are too uptight. They never hallucinate, their logic is airtight, but they require a level of rigor that makes mathematical discovery feel like drafting legal contracts. Every statement must be precise down to the last quantifier. That's great for verification but disastrous for exploration, where you often prefer a "roughly correct" wild idea over a precisely formulated, mundane one.

By combining discovery to formal mathematics, the model is enabled to think outside of the box. Let’s add some mad scientist vibes.

Many mathematical problems are really optimization or constraint satisfaction puzzles: maximize some quantity under conditions, or find exceptional objects satisfying many criteria simultaneously. Find the largest graph with no four-cycle. Build Hadamard matrices where every column agrees on exactly half its entries—all 1s and -1s, perfectly balanced. These aren't proofs – they're constructions. And the search space explodes quickly.

We developed PatternBoost to attack these problems. The idea is simple but powerful: generate lots of random solutions, keep the best ones, train a model to recognize what makes them good, and then use that model to generate better solutions. Repeat and break records.

We found counterexamples to completely disprove a 30-year-old graph theory conjecture this way. Since then, by applying Patternboost, we've generated hard-to-compute objects in high-energy physics – collision events with many jets – that physicists struggle to simulate. We've also built special triangulations of four-dimensional polytopes for string theorists classifying Calabi-Yau manifolds.

The magic ingredient of these approaches is that good solutions really do have "something in common." Even when we can't articulate what that is, models can learn them.

For many mathematical problems, no general solution method exists. We can solve particular instances – the easy cases, the small-sized examples – but each new problem requires ingenuity and trial-and-error. What if we could train models to translate problems directly into solutions?

The approach is to train on problem-solution pairs. Sometimes we work forward from problems we already know how to solve. Often we work backward – pick a random solution, then construct a problem it solves, a task that's frequently simpler than the reverse. Fine-tune on the special cases where we have techniques.

We applied this to a 130-year-old challenge: discovering Lyapunov functions for dynamical systems. Since 1892, we've known these functions control global stability – they guarantee that solutions stay bounded rather than diverging to infinity. But no general method exists to find them for arbitrary systems. By a wide margin, we discovered new Lyapunov functions that beat state-of-the-art methods, applying the translative method. The work automated mathematical creativity in domains where we've been stuck for over a century.

These “translation tools” can also be used for discovery in a different way. Sometimes, translative models help find intuitions. Train multiple models with slightly different parameters on the same problem and compare model performance. One may uncover unexpected properties of the underlying problem. 

We’ve done this to bootstrapped amplitudes – fundamental objects in theoretical physics. By training models to predict one half of an amplitude symbol from the other, we found surprising regularities in their performance that pointed to new physical intuitions.

We've also applied this to predicting the Frobenius coefficients of elliptic curves. Experiments point to yet unknown relations between the parity of successive coefficients. These experiments are easy to automate – we've previously released an open-source framework called Int2Int for exactly this purpose.

Pre-training is a common technique for building language models. Models are first trained, unsupervised, on vast amounts of text. In this initial phase, they acquire language proficiency and learn general information about the world. Then, the model is fine-tuned on specific tasks. It is generally accepted that pre-training is key to emergent properties of LLMs: models become capable of performing tasks they would not have learned if trained on the final tasks alone. This is a consequence of models learning deep representations of language during the pre-training phase.

What if we did the same for specific families of mathematical objects? We call this approach "mathematical world models." Train a model on multiple tasks that all take the same mathematical object as input – say, a graph. Use a shared encoder to build a common representation, but task-specific decoders for different outputs. Unlike language model pre-training, this would be supervised: the model learns from labeled examples across many tasks simultaneously.

The goal is to learn a universal representation of the mathematical object – say, characteristics of the graph – that makes it easier to learn harder tasks later. These encoders could be built for different mathematical objects and then reused and composed like building blocks.

Understanding what representations these models learn may provide new insights about the mathematical objects themselves. A special bonus.