A Fields Medalist Stuck for Two Hours. AlphaProof Climbed for Three Days.

On *No Priors*, Sarah Guo and Elad Gil talk with three people from Google DeepMind's AlphaProof team: Thomas Hubert, Rishi Mehta, and Laurent Sartran. AlphaProof is an AI system that finds and verifies mathematical proofs, building on DeepMind's earlier work in chess and Go. At the 2024 International Mathematical Olympiad, the oldest and most prestigious contest for young mathematicians, it solved four of six problems, a result the team later described as silver-medal standard under that year's marking. Some of those solutions arrived in minutes. Others took three days.

The three guests arrived by way of games. Rishi Mehta, one of the technical leads, is a chess player who read the AlphaZero paper, watched the games, and wanted to work on something beautiful, superhuman, and almost alien. Laurent Sartran spent early years on malware detection and ad targeting, then on AI research, with a constant interest in systems that spend more compute to think harder; math looked like a perfect domain. Thomas Hubert played Go instead of learning to program at ten. Building a computer Go program was his father's dream. He followed that trail to DeepMind, then through AlphaGo, AlphaZero, MuZero, AlphaCode, and AlphaTensor.

Hubert's path into math was already sitting on two results. AlphaCode had shown that models could generate a lot of good code, and mathematics offered something games do not: perfect verifiability. Transformers were already changing how the work got done. Formal math looked like the natural next place to put an AlphaZero-style loop.

Board games always have an opponent. That is what made self-play so powerful in AlphaGo and AlphaZero: the agent always faced someone exactly as strong as itself. Mathematics has no opponent. You just have to think. Hubert calls it almost purely cognitive. You cannot run an experiment in the world. Mathematicians joke that a nap helps, because the unconscious keeps working. Confronted with a really hard problem, the live question is how you go about trying to solve it at all.

Architecturally, AlphaProof is AlphaZero with the pieces renamed. Hubert describes three components: a neural network for intuition, large-scale reinforcement learning from trial and error, and a planning search that looks, in the current situation, for the best next action. If you can handle infinite action spaces, the action does not have to be a chess move. It can be a line of a proof. That is the first change. The second is to write the math in a formal language, which is another way of saying they use code to write mathematics. Lean is the popular example. Once a proof is complete, the machine sends back a signal: correct or not. Correct proofs train a better network, which then tackles harder problems. Self-play's opponent is replaced by a verifier.

The search space is wildly larger than chess. People imagine writing a proof as picking at each step from a bag of known tricks. Many proofs instead require you to invent a function out of thin air, or to rewrite an expression in one of infinitely many ways, only a few of which make progress. Some problems wait decades for a new theory and an entirely new angle. That, Mehta says, is why statements a child can read have stood unsolved for centuries: the search space is not easy to navigate.

IMO problems come in four categories: algebra, number theory, combinatorics, and geometry. AlphaProof is strongest at algebra and number theory, weaker at combinatorics though still capable on some contest problems, and was not applied to geometry in 2024. Elad Gil asks what it would take to grow from here, including whether some areas simply need new forms of training data. Mehta's answer for how the agent navigates the huge space is an idea the team named test-time RL.

When the base network searches and cannot find a proof, the agent constructs many variations of the problem in the vicinity of the original and tries to solve all of them. Any variant it cracks becomes experience. The network improves a little, then a little more, and hill-climbs toward the original. Mehta compares it to a new scientific question where your priors from other problems do not apply. You have to design bespoke experiments on this problem itself, learn something, and climb. The IMO questions that took three days were this loop: cannot solve it, propose variants, get slightly better, repeat, for days of inference-time compute.

Put those three days back in context. Against a human exam clock they are a gross overtime. Against a research clock they are fast. A mathematician stuck for three months is ordinary. AlphaProof stuck for three days and climbed out.

Asked what would raise performance dramatically, the team names a missing skill first: theory building. AlphaProof does not invent theories. Equipped only with what it has, it would not come up with the complex analysis needed to derive results in number theory. Generating variants and getting better by solving them lets it tackle the original problems of interest. Building the toolbox those variants live in is another job. Hubert thinks that capability is required to go much further, toward something like the Riemann hypothesis. Either it emerges, because harder proofs already force you to introduce new mathematical objects to decompose a problem, a hint they already see at IMO scale, or the team will have to think explicitly about how to encourage theory building.

The second bottleneck is translation, especially combinatorics. Those problems can be stated in an obfuscated way. Sartran's example is counting: forty socks in a drawer, how many pairs, asked crookedly, is already awkward to put into Lean. Part of the difficulty is that the library does not contain the tools you need. If you had objects that expressed what an agent is, what an environment is, what a strategy is, many combinatorics problems would be much easier to state. Because those objects are missing, autoformalization would have to invent definitions, objects, and their properties before it could even formalize the question. That loops back to theory building.

Gil asks whether there is a Turing-test equivalent for the field, in the spirit of Hilbert's 23 problems in 1900, which defined much of twentieth-century mathematics, or the seven Millennium Prize Problems, of which one has been solved. Hubert says the brain thinks linearly and AI experience says to think exponentially, because things can change quickly. At the same time, nobody knows how hard the Riemann hypothesis is: two orders of magnitude, three, maybe ten. Without an existence proof you cannot even estimate. Solving it will involve brand-new math. Guo reminds listeners that the hypothesis is about the distribution of primes. How far AlphaProof is from that, they will not pretend to know.

Why spend a career on math at all? Hubert, not a mathematician, offers two reasons. It has been called the language of the universe, sitting at the core of the technology we use, so understanding it is a way of understanding the present world. Solving it also demands reasoning, generalization, and abstraction, the skills people talk about when they talk about cognitive AI. The domain is constrained and the complexity is unbounded, which makes a focused effort look worthwhile. Sartran's motive is more engineering: he has chased systems that get better by thinking more, in machine translation, text diffusion, and navigating agents. Proving statements looked like one of the last big challenge domains still open, and the next step of thinking more is thinking so much that the agent grows its own theories.

Mehta's reason is closer to pure search for truth. A large number of people already pursue these problems with no application in mind. They want to know why a thing works this way. Solving the Riemann hypothesis has that flavor. History is full of theory developed for its own sake and used later: number theory in cryptography and zero-knowledge proofs, group theory in quantum mechanics. Hubert has been reading about the Langlands program, described to him as a unified theory of mathematics that might connect number theory and geometry the way physics looks for a unified theory. He likes the abstractions even when he does not fully understand them, and he wants to learn what mathematicians actually care about, knowing they will disagree. Mehta notes that Bombelli was ridiculed for imaginary numbers; years later they were needed to describe alternating current. If a machine can develop its own theorems, where you point it is a genuinely open question.

The application Sartran is most excited about is code verification. Software today is written, tested, and shipped when the tests pass. Bugs and security issues still slip through. In avionics and cryptography, people already write down the properties an algorithm must satisfy and prove them in code, by hand, because the domains are too critical not to. If specialized tools removed the human bottleneck of writing those proofs, verification could become common and the software industry would be in a much better place. Mehta is also excited about transfer: the mathematical reasoning skill itself, and the technology of scaling RL and spending a lot of inference-time compute, both look portable to other problems.

Guo asks the unformalizable case: can an RL agent make something funnier, given that it is easier to tell if a joke lands than to write a standup set? Hubert's split is about where the reward comes from. Some domains have ground truth; humor is a fuzzy human concept, and aliens might not share it. Humans are the grounding there, the real world is the grounding in others, and machine checking is the grounding in math. The RL framework still applies. What does not transfer is the scale. Machine-checkable rewards can run far past what you can ask of people. Humor, where everyone gets a say, still has room to scale, just not like Lean.

Gil asks whether unlimited access to Terence Tao for labeling would even be useful, versus just doing more search. Sartran's first answer is about style. AlphaProof discovers its own proofs, learns from the valid ones, and has developed a style outsiders have called quite alien. Unlimited Tao would produce correct proofs with a human sense of niceness, and you could optimize among valid proofs for ones that look nice, for interpretability and for teaching. Guo hears a slightly damning claim: that is preference, not capability. If the proof is correct, why care that it looks alien? Sartran agrees interpretability is not the only use. With more supervised data you could skip exploration, translate every proof known to humans, make the agent much better, and save years of compute.

Mehta puts the specialist data and the RL data in sequence. Small amounts of precious human data seed the agent, taking it from a complete zero to a place where it can play the environment efficiently. From there, RL can match or exceed the human, with its own style. He thinks that is the general path for RL on large language models: expert data turns a pile of weights into something surprisingly strong, then RL takes it to superhuman. Guo adds that Poincaré is often called the last person who understood all of mathematics. An AI that could encapsulate the subject in a single program might check proofs in side fields where almost nobody is left to referee.

Mathematicians do not have access to AlphaProof today. Hubert is modest: they cannot rival Tao at all. What they have shown is that you can learn general mathematics almost from scratch and reach an impressive high-school contest level. The knowledge base still has to grow before the system is useful. Tao, in interviews over the past year, has noted that math papers still have one, two, or at most five authors, because checking other people's work is too time-consuming for larger teams. If a formal system checks everyone, you could work like astronomy: an amateur living nowhere you have been, whom you have never met, submits a proof, and you trust the machine rather than the stranger. That is a way to scale collaboration among humans, and between humans and AIs. For now the team would rather be a graduate student. They are not especially good at asking the right questions. They want the community to hand them the ones that matter.

Guo, a Go player herself, asks for an alien move. Hubert puts IMO 2024 problem 6 on the screen. Problems 3 and 6 are supposed to be the hardest each year; this one turned out to be one of the hardest ever. Only five of more than 500 contestants solved it. The contest was in Bath, and the problem invents a tongue-in-cheek name, aquesulean, from the town's Roman name Aquae Sulis. Two equations characterize such a function. You must show there exists an integer C such that for any aquesulean f, the expression F(R) + F(-R) takes at most C different rational values, and you must find C. The standard attack is to prove an upper bound and a lower bound and make them meet.

AlphaProof had already proved C is at most 2, a result the team published in full on the DeepMind blog. The remaining question was whether C is 1 or 2. Showing it can be 1 is trivial. Showing it is 2 requires exhibiting a specific function for which that even-looking expression actually takes two different values. Timothy Gowers, a Fields Medalist and one of the judges, tried for a couple of hours and could not find the construction. Hubert is quick to say this does not mean AlphaProof is better than Gowers at math. It means that step is genuinely hard. The agent produced f(x) = -x + 2⌊x⌋, a jagged function built from the floor. Plug in R = -1 and R = 1/2 and you get two different values. C is 2. In Mehta's view it may be the hardest problem AlphaProof has ever solved.

Advice for people who still spend their days on math: learn Lean early. Formal math is becoming a medium of collaboration, still a minority, a growing one, and AI will only accelerate it. It is also an educational tool. Informal proofs are written at the author's level of abstraction; a step marked trivial comes with no explanation. A formal proof lets you zoom to the detail you need. On paper, the pain is not knowing whether you have fooled yourself, and waiting in line for a teacher. In a formal language the machine tells you what is left to prove. Sartran, speculating, splits mathematicians into theory-builders and theorem-provers, noting that proving sometimes requires building, as with Fermat's Last Theorem. There looks to be more room for human creativity, taste, and skill on the theory-building side.

Guo finds "go develop good taste" a much harder assignment than "learn Lean," and also more valuable. Tao's taste in problems, arithmetic progressions of primes, dragged a whole set of methods and tools into existence. Mehta's closer is the line he had seen elsewhere: as machines get better at finding the answers, we will have to get better at finding the questions. These systems have no notion of what is interesting, or of how to break a large question into smaller ones that might be. He already feels that as a software engineer. More and more the job is not the low-level details. It is making the high-level decisions the tools can help with.