TLDR: As AI systems get better at proving hard theorems, “number of important open problems solved” may become a worse proxy for mathematical progress. My concern is that proof production could become much cheaper than the harder-to-measure work of building abstractions, connecting ideas, and improving our conceptual map of mathematics. If we keep rewarding the easiest thing to count, we risk Goodharting the field.

---

There is an interesting way to add points on an elliptic curve. In the usual picture, you draw a line through two points, find where it intersects the curve again, and reflect that third point across the horizontal axis. With the appropriate treatment of special cases, this defines addition.

But why should it be associative? Why should (A+B)+C=A+(B+C)?

One approach is to write down the coordinate formulas, substitute everything into everything else, and verify the resulting identities. It works. It is also, as Andrew Sutherland’s lecture notes put it, “a tedious task that does not yield much insight.”

Another approach is to connect the curve to an algebraic structure called a class group. Assign each point a distinct class, show that the geometric construction agrees with the class-group operation, and associativity follows. This is essentially the approach used in Lean’s mathlib, which maps the points into the ideal class group of the curve’s coordinate ring.

The important discovery is the correspondence: this geometric recipe is an instance of an algebraic operation we already understand. Rather than checking that two complicated expressions agree, we identify a structure that explains their agreement.

I think this distinction is a useful starting point for thinking about something that has been bothering me increasingly in AI and mathematics.

* * *

On September 8, OpenAI announced a proposed solution to the Navier–Stokes Millennium Prize problem, accompanied by a writeup and a Lean formalization. Three days later, a group of Fields Medalists published an open letter arguing that the push to solve mathematical problems as benchmarks risks confusing problem-solving with conceptual understanding.

My friend Isabel’s response (Of course it hurts) questions whether the mathematical community’s existing incentives actually reflect those stated values, and what should change as AI becomes more capable. Reading her post and the letter motivated me to try to make sense of an ick I’ve had for a while.

I spent three years studying mathematics full-time, later did research on AI for mathematics (autoformalization and automated theorem proving), and now do AI safety research. So this touches on several things I care about.

In short, what worries me is the possibility of getting much better at proving things while treating that, by default, as getting much better at mathematics.

Proof as a proxy

More than the accumulation of true statements, a large part of what I value in mathematics is finding a representation in which previously difficult or disconnected things start making sense together.

One way to think about this is compression. Instead of treating many arguments as separate objects, we find a common structure from which they follow.

Historically, solving a sufficiently difficult problem was often evidence that someone had developed new machinery, found a better abstraction, or established an unexpected connection. Proving the theorem was the visible achievement, part of its significance lay in the conceptual work needed to get there. In that sense, it was a useful proxy for something harder to measure.¹

Grothendieck’s reconstruction of algebraic geometry is an example on a much larger scale. Building on earlier work and working with others, he developed schemes and cohomological machinery that reorganized the subject. Schemes, for example, allowed equations over different number systems to be studied within a common geometric framework. The contribution was not merely a collection of new results: it changed which problems could be seen as instances of the same underlying structure.

I find the software-refactoring analogy useful here. You can add functionality by handling each new case separately. Or you can reorganize the code around a shared abstraction, so that those cases no longer require independent implementations.

A refactor can be substantial progress even before it adds a new feature. Some mathematical advances look similar: their importance lies partly in reorganizing the problem space, not in closing one particular open statement.

What AI changes

I’m not claiming AI can’t become good at finding abstractions or doing the right refactoring. It could plausibly become much better at this than humans. But proof production could become dramatically cheaper without a corresponding increase in the conceptual work we get out of it.

Suppose a system can search through enough possible arguments to produce correct proofs of difficult statements, but leaves us with little reusable beyond those particular derivations. It has achieved something real: we know things we did not know before. What it has not necessarily done is give us a better way to understand the subject.

When AI allows us to close problems without finding much reusable structure, “this hard conjecture has been proved” becomes a weaker signal of the broader mathematical progress that used to often accompany it.

This should not be simplified to “human proof beautiful, machine proof ugly.” The distinction is between different kinds of mathematical contribution, regardless of who (or what) produces them.

When the proxy becomes the target

This matters because the field of AI has a recurring habit of benchmark-maxxing.

We choose a benchmark because it correlates with some broader capability we care about. Then we optimize aggressively against it. Number goes up. Eventually it becomes less clear how much of the improvement reflects the broader thing and how much reflects getting extremely good at the measurement itself. This is the basic Goodhart problem.

Open problems in mathematics are a very sexy benchmark. There’s a simple success condition: yesterday we did not have a proof, today we do. And solving a famous one carries enormous prestige.

The default trajectory is therefore easy to imagine: AI labs race to close increasingly prestigious open problems, because those wins are unambiguous and legible. Academia follows the attention. More compute, funding, and status flow toward producing the shiny last step: “X is now proved”.

Maybe the proof is a huge AI-generated Lean derivation with little new conceptual machinery behind it. That does not make it worthless. But it is much easier to reward “this famous conjecture is now proved” than to reward the slower, less legible work of building theories, finding abstractions, integrating results, or deciding which questions are worth asking in the first place.

The incentives in mathematics are already questionable here. AI could amplify them considerably: the part of mathematical work that is easiest to benchmark could also become the part we invest most heavily in.

The resulting failure mode is that we get much better at extending the set of things we can prove, without getting proportionally better at organizing, connecting, or understanding them.

The frontier expands, but the map does not get much better.

There is a human consequence too. If the field continues to reserve much of its highest prestige for being the person who closes the famous problem, while that is precisely the step AI becomes best at scaling, it is not difficult to imagine mathematicians feeling increasingly disempowered. The remaining work may be intellectually crucial while still being treated as secondary.

* * *

I do not claim to have a complete objective function for the field of mathematics. I also do not think we need one before recognizing that theorem solve-rate leaves a lot out.

Compression is just one example of something theorem counts fail to capture. Mathematical progress has many dimensions, and part of the challenge now is figuring out which signals we want to preserve as proof itself becomes cheaper. That will likely not reduce to another clean benchmark, but difficulty of measurement is not a good reason to let the easiest thing to measure become the objective.

We should absolutely build systems that can prove difficult theorems. As they get better, though, “how many previously open statements can they close?” should remain a capability we measure, not become our definition of progress in mathematics.