Mathematics is Much More than Proof

The automation of mathematics has been going on for more than a century. If AI can automate some or all parts of mathematical proof, that will be another important phase in this process, but not the last. While mathematicians sometimes elevate proof as the essential part of their discipline, there remain profound parts of mathematics that sit above proof, as proof sits above mere calculation. Until AI can learn which questions to ask and to invent entirely new mathematical fields, there will be deep work in mathematics that only human mathematicians can do.

Frontier AI systems can now prove mathematical results that matter. We first saw a flurry of proofs of minor conjectures in early 2026, then a disproof for the well-known Unit Distance Conjecture in May, and most recently OpenAI’s set of 10 proofs in mathematics and computer science in August. We’ve rapidly gone from an ability to prove some obscure conjectures to important proofs for theorems of interest to many mathematicians.

In the wake of results like this, many people — including many mathematicians — have suggested that the days are numbered for human mathematicians. I think they are jumping the gun. This is because proof is but one part of mathematics, and not, in my view, the most interesting part. Even if AI completely automated proof, doing it far better than any human at a tiny fraction the cost, deep, important, and fascinating parts of mathematics would remain.

Many kinds of work in mathematics

Mathematics involves many different kinds of activity, some of which have already been automated.

Numerical calculation was a central activity of mathematicians for thousands of years. Eminent mathematicians spent something like half their working lives performing numerical calculations. This core function of mathematicians was completely automated during the 20th Century with the advent of calculators and then computers. We now think of this as freeing mathematicians from immense drudgery, allowing them to spend their time on more interesting and important parts of mathematics.

Symbolic manipulation is also a key activity. Think of things like solving equations, or finding the integral of a function — where there are a variety of allowed steps that can be combined in different combinations to produce a vast web of subsequent formulas. Finding one’s way through this web to an expression of a desired form (e.g. simplified, or factored, or expanded, or with the variable $x$ isolated) is something almost everyone has experienced in mathematics classes. But over the last 40 years, tools such as Mathematica, Maple, and Wolfram Alpha have largely automated this kind of work. While such symbolic manipulation is more interesting than numerical calculation, tools to automate it have largely been seen as a positive for mathematics, or (more commonly) completely unremarked upon.

Proof is another important kind of activity. Mathematicians attempt to find watertight arguments establishing the truth (or falsity) of a mathematical statement. While the public often see mathematics as calculation or symbolic manipulation, many mathematicians see proof as being much more fundamental to mathematics — what separates it from the empirical sciences and gives it its distinct character. Proof is now in the process of being automated, and it has become clear that even if AI progress were to stall out very soon, AI-discovered proofs will be an important part of research-level mathematics. Whether there will be a long ‘centaur’ period where the best proofs require contributions from both humans and AI is currently debated.

But these are not the only kinds of work in mathematics, and not (to my mind) the most important.

Asking the right questions

Proof takes a formal mathematical statement and shows how it follows logically from other mathematical statements (which are either taken as axiomatic, or have already been proven). Proof shows what follows from what and (more often than not) why.

But on its own, it isn’t enough to make progress in mathematics. The number of formal statements that one could attempt to prove explodes exponentially with the length of the statement. The number of different mathematical statements that could be expressed in a statement that fits on a single line of a journal page is more than the number of particles in the observable universe. Even a machine that could prove any true mathematical statement in a microsecond would never get up to considering the unit distance problem before all the stars have burnt out. And that is despite the unit distance problem being remarkably concise.

To make progress in mathematics, we therefore need to be able to ask the right questions. We might think this is a matter of the ability to consider a mathematical question and judge how interesting or important it is. But even if we could automate that, it wouldn’t be enough — for there isn’t enough time to even consider for a microsecond each of the questions one could ask. Instead, one needs to be able to home-in on the important questions without even generating a minuscule fraction of the unimportant ones. This is clearly possible, as human mathematicians do it. But such a capability hasn’t yet been demonstrated for AI systems.

I’m not saying that today’s AI systems definitively can’t do it. It is more that there is very little evidence either way. A key issue is that we don’t have good benchmarks to measure their success at asking the right questions. But this also means we don’t have good training data (or a good verifiable reward) to teach this skill to AI systems. Unless it has come for free when pre-training on mathematics texts or while learning to prove statements during reinforcement learning, it is hard to see why they would possess the skill of finding good questions. I’m sure people can already make language models that spit out large numbers of mathematical questions and conjectures, but I’m doubtful about their quality.

Working out which questions to ask in mathematics plays a similar role to hypothesis generation in science. Most accounts of the scientific method focus on the key role of experiment which allows us to eliminate incorrect hypotheses. But they don’t say enough about how scientists manage to find the hypotheses worth testing in the exponential forest of mediocre hypotheses. In both cases, generating a good question/hypothesis is crucial, and is where much of the work lies.

In fact one can somewhat quantify the sense in which finding the right question can be half of the work (or more). The amount of information in a yes/no question (such as a conjecture or hypothesis) is equal to the number of bits in the proposition that is being questioned, minus 1.$^1$ You can see this because if you take a yes/no question and add its answer (a single bit), you get that proposition (e.g. the theorem). Similarly, the amount of information in a question looking for a particular kind of thing (an object meeting some condition, or a proof) is equal to the number of bits in the proposition minus the number needed to specify that thing. So there can easily be a lot of information already embedded in the question.

Another way to think about the value of questions is that they are known unknowns. They isolate and make explicit a very particular piece of our ignorance. Good questions are those that pick out a proposition whose truth or falsity would be important to know, especially if it wasn’t previously clear this was a gap in our knowledge.

Opening new fields of mathematics

To my mind, the most important work in the history of mathematics has not fallen into any of the above categories. It has been the discovery of new fields of mathematics; work that has given mathematicians new language and new concepts allowing new kinds of mathematical questions to be asked.

With the development of probability theory in the 17th Century, mathematicians became able to ask (and answer) questions about the probabilities of different kinds of events. Concepts like probabilities, expectations, independence, distributions, and variance entered their vocabulary. There was nothing fundamental preventing this from being invented in antiquity, but until it was developed, there was no way of even formalising questions about these concepts.

The 17th Century also saw what may be the most important unification in the history of mathematics. Previously geometry and arithmetic were seen as two distinct domains of mathematics, proceeding in parallel for thousands of years. Descartes found a way to unify these two realms into the new field of algebraic geometry,.

The 19th Century saw three dramatic changes to our conception of geometry. For the first time, mathematicians explored the geometry of higher dimensions (4D space and beyond), allowing us to ask questions such as how many platonic solids exist in $n$-dimensions, and how much of the space inside a higher dimensional sphere is located near its surface. They also showed how relaxing the fifth axiom of Euclidean geometry allowed one to study the geometry of curved spaces, such as the surface of a sphere. And they considered the geometry of fractal curves, which would go on to be interpreted as fractional dimensions.

These were profound conceptual expansions of geometry that allowed one to think about entirely new kinds of objects and spaces. And stunningly, they were all eventually found to be relevant in understanding the world around us. Our spacetime is a curved 4D space. And our rivers, coastlines, and blood vessels obey the rules of fractal geometry. Surprisingly, none of these developments required advanced pre-requisites. The key ideas of these fundamental expansions of the nature of geometry could have been explained to Euclid with an afternoon spent drawing figures in the sand. Yet it took another two thousand years for someone to conceive of them.

There are many other examples too of how mathematicians have opened up new vistas. Others include calculus, set theory, Cantor’s treatment of the infinite, proof theory, theory of computation, and information theory.

Each new field allowed entirely new kinds of questions to be asked and answered. To my mind proving theorems within a given field fairly quickly runs into diminishing returns. After the first few decades, many of the theorems that are both profound and approachable have been proven. But opening up new fields renews these possibilities.

Where we stand

While current AI systems are starting to automate mathematical proof, there is currently very little evidence that they can ask powerful questions or find profound new fields of mathematical enquiry.$^2$ AI may well come for these areas too, and this may happen very swiftly. My point here is not to say that there will forever be some special areas where human mathematicians reign supreme. Instead, I’m trying to point out that the automation of proof alone would not be the end of mathematics.

Some mathematicians have suggested that after proof is automated, human mathematicians could still add value through explaining the great works of AI mathematicians. While I actually think this kind of translational work is very valuable and underrated in academia, one can’t help feeling that from the perspective of mathematicians, this would be very much a demotion. What I’m suggesting here is that there are other key parts of mathematics they could shift their focus to — asking deep questions and developing profound new fields of mathematics — where there is still a comparative advantage for humans, and would be more like being promoted to a position where they can focus on setting the direction and vision for their discipline.

$^1$ This is actually a lower bound — when we aren’t exactly 50-50 about whether the answer is true or false, the question is missing even less than 1 bit. This is one way to see the difference between a conjecture and a question. A conjecture is where one side seems more likely and so contains slightly more information than a question (though less than 1 bit more). While mathematicians often focus on conjectures rather than questions, I think questions are the more fundamental entity and are somewhat neglected in the practice of mathematical research.

$^2$ There are other important kinds of mathematical work too, such as finding powerful new methods and powerful new abstractions; finding new kinds of mathematical objects and new ways of seeing old ones.

23 August 2026