We Need a Stockfish for Math
LLMs have become shockingly good at math. They solve competition problems, assist with research, and are improving fast enough that some fear human mathematicians are becoming marginal. I want to make the opposite critique: LLMs aren’t nearly good enough at math, and the way we’re pursuing the problem almost guarantees they never will be.
The Chess Analogy
Imagine an alternative present in which chess engines were never invented and the world’s best players are still human grandmasters. In this world, the first programs ever to beat people at chess are LLMs like Claude and ChatGPT.
LLMs aren’t exceptional chess players, but they’re respectable. On current leaderboards, frontier models play at roughly 1500 Elo. Nowhere near Magnus Carlsen, but decent. More importantly, they’re improving: more data and more compute reliably make them stronger. In our alternative world, it would be natural to extrapolate the trend and conclude that LLMs will eventually become the greatest chess players of all time. After all, they’d be the only machines we’d ever seen play the game at all.
But we don’t live in that world. We live in a world with Stockfish, which crushes grandmasters and LLMs alike. This should surprise no one. Stockfish was designed from the ground up around the structure of chess: it efficiently searches the space of possible moves using clever algorithms and learned heuristics. For an LLM, playing decent chess is an incidental byproduct of predicting text. For Stockfish, it is its entire reason for existing.
LLMs Are Not Math Engines
LLMs are our first experience with computers that can attempt a wide range of math problems. Computers have long been helpful with specific proofs, but LLMs are generalists: they usually fail to prove things, occasionally succeed, and are steadily improving.
That upward trend tempts mathematicians into the same fallacy the chess enthusiasts of our alternative world would have made: treating LLM progress as evidence that LLMs are the way to get computers to do mathematics. Under this view, when an LLM fails to solve a problem, the remedy is always the same: more compute, more training data, and hope.
But LLMs are not math engines. They were not built from the ground up to prove theorems the way Stockfish was built to play chess. Stockfish’s power flows from a deep understanding of its game, translated into theory and algorithms. Theorem proving is admittedly far less well understood than chess, but that is exactly the problem. Scaling LLMs brings us no closer to understanding the nature of theorem proving itself.
What We Actually Want
The real goal is to make computers solve math problems. We want to automate problem solving and logical reasoning. “Get LLMs to solve math problems” is a needlessly restrictive framing of that goal. It is entirely possible that LLMs, or even machine learning in general, will play no part in the best solution. AI labs like Anthropic and OpenAI will naturally frame the goal around their models; that’s their business. Mathematicians who care about automating mathematics should not inherit that framing by default.
And we don’t just want a program that proves theorems, we want the best one. That requires knowing what “best” means. In my view, an ideal automated theorem prover (ATP) should satisfy three criteria:
- Soundness. It must never prove something false. Without this guarantee, we could never fully trust its output.
- Completeness. If a proof exists, the prover must eventually find it. Finding proofs is, after all, its job.
- Efficiency. It should waste no time or resources in its search. A brute-force enumeration of all possible proofs might be sound and complete, but it would never be useful.
LLMs fail all three. They come with no soundness guarantee and produce incorrect proofs constantly. They are not complete since they routinely fail to prove true theorems. And there is no reason to believe they are efficient, because efficiency at proof search was never a design consideration. LLMs are steadily improving at math, yet we are no closer to satisfying any of these criteria.
One might object that humans fail all three criteria too: we publish flawed proofs, give up, and waste enormous time. True, but why should machines inherit our failures? LLMs are trained to imitate human problem solving. The point of automation has always been to surpass human capability, not to replicate our limitations at scale.
The Gödel Objection
People often assume these criteria are impossible to satisfy, usually by appeal to Gödel. This rests on a confusion. The incompleteness theorems constrain formal systems: a sufficiently powerful, consistent system cannot prove every true statement. They say nothing that prevents a theorem prover from being sound and complete relative to such a system. Indeed, theorem proving is semi-decidable: if a proof exists, there is a procedure guaranteed to eventually find it. Gödel limits which statements have proofs; he does not limit our ability to find the proofs that exist.
A fair criticism, however, is that soundness and completeness are formal properties. If we wish to design an ATP that outputs natural language solutions to problems, it’s not entirely clear how soundness and completeness are measured in the domain of natural language.
The Future
It’s genuinely valuable that researchers and companies are exploring how good LLMs can get at math, and their progress is impressive. But “how good can LLMs get?” was never the question of automated theorem proving, and in my opinion, it isn’t a particularly interesting question either.
Approaching automated theorem proving from first principles teaches us about the problem-solving process itself, and about the foundations of mathematics. Distilling the immensely complex machinery of human logical reasoning into an algorithm is no easy feat, but it is also one of the most important problems of all time.
It is unfortunate that the vast majority of funding and effort goes toward “how do we get LLMs to solve math problems,” while the more fundamental question of “how do we get computers to solve math problems” has fallen by the wayside. Good work continues: theorem proving in type-theoretic languages like Lean keeps advancing, and SAT solving has made impressive strides. But this area deserves far more attention than it gets.
Two obstacles have long held ATP research back. The first is perceived impossibility: until the advent of LLMs, the math community as a whole never seriously entertained the idea that computers could help with hard problems. The second is a lack of raw material: only recently have vast corpora of mathematics been formalized, and without formalization there was little foundation on which to build proof-search algorithms. Both obstacles are now falling away, and the future looks bright.
We need a Stockfish for math. We shouldn’t settle for anything less.