Can a model do math it doesn't understand?

Suppose a model hands you a Lean proof of a theorem, and Lean’s kernel accepts it. The proof is correct. That part is not up for debate, because a proof checker is about as close to an objective referee as mathematics has. What is up for debate is whether anything “understood” the theorem along the way, and whether that should change how you feel about the result.

The question connects older arguments about minds and formal mathematics with newer experiments on what models compute. I want to work through those connections without treating the experiments as a solution to the philosophy.

For my own research, I find “can it tell when it’s wrong?” more useful than “does it understand?” It gives me something specific to test.

The Chinese Room, restated for proofs

John Searle’s paper “Minds, brains, and programs” came out in Behavioral and Brain Sciences in 1980.¹ The setup is simple. Searle imagines himself locked in a room with a rulebook, written in English, for manipulating Chinese characters. Questions in Chinese come in through a slot. He follows the rules, pushes the right characters back out, and to the people outside his answers look like those of a native speaker.

His verdict on himself: “I do not understand a word of the Chinese stories.”¹ He produces the answers, in his words, “by manipulating uninterpreted formal symbols.”¹ And since a computer running the same program is doing exactly what he is doing, he concludes that the computer understands nothing either. The target was what he called “strong AI,” the claim that a programmed computer literally has a mind and that the program explains human understanding.

Now swap the Chinese stories for a theorem. The input is a statement in Lean. The output is a sequence of tactics. The rulebook is billions of learned weights instead of a ledger. Lean checks the output and says yes or no.

This isn’t hypothetical. In July 2024, Google DeepMind’s AlphaProof, a reinforcement learning system that writes proofs in Lean, solved three of the six problems at that year’s International Mathematical Olympiad, and together with AlphaGeometry 2 reached 28 out of 42 points, a silver medal score.² Its proofs were formally verified, so their correctness wasn’t in question. Some problems took it up to three days.² So the Lean room exists, it outputs correct proofs, and the old question applies to it directly.

One thing is different from Searle’s version, and I think it matters. In the Chinese Room, the people outside can only judge whether the answers look right. In the Lean Room, the referee checks every step. Searle’s room could fool you. Lean checks a formal derivation against a formal statement. People still need to check that statement, its assumptions, and any added axioms.

The systems reply, and Dennett

Searle anticipated objections, and the most famous is the one he labeled the “systems reply,” which he attributed to Berkeley. It goes: fine, the man doesn’t understand Chinese, but he’s just one part of a larger system that includes the rulebook, the scratch paper, and the data banks, and the system as a whole understands.

Searle’s answer is to fold the system into the man. “Let the individual internalize all of these elements of the system,” he writes: memorize the rules, do every calculation in his head.¹ Then there’s nothing in the system that isn’t in him, and he still doesn’t understand Chinese, so neither does the system. He adds that he feels “somewhat embarrassed” to even give this answer, because he finds the systems reply implausible to begin with.¹

Daniel Dennett spent decades on the other side. In his original 1980 commentary he called the argument “an intuition pump,” a thought experiment built to pump out an intuition rather than establish a conclusion.³ His sharpest point, developed in “Fast Thinking” (1987), is that speed is “of the essence” for intelligence.³ A man shuffling paper would be absurdly slow, and our intuition that nothing in there understands may be partly an intuition about that slowness. Dennett held that programming “is precisely what could give something a mind,” the exact opposite of Searle.³ By 2013 he was calling the Chinese Room “clearly a fallacious and misleading argument.”³

Reading the two side by side, what strikes me is that neither of them ever settles the dispute with evidence. Searle says the room obviously lacks understanding. Dennett says that’s an artifact of how the room is described. The argument is about what the word “understand” refers to, and they disagree on that before any experiment starts. The Stanford Encyclopedia entry, which is long and fair, works through many replies and counter-replies over four decades without declaring a winner.³

The disagreement makes me cautious about using “understanding” without first saying what would count as evidence.

Hilbert and Brouwer had this fight first

Here’s the part I didn’t expect when I started reading. Mathematicians had their own version of “symbols versus meaning” sixty years before Searle, and it was about human mathematics, not machines.

David Hilbert’s program, which he proposed in 1921, aimed to put all of classical mathematics into a formal axiomatic system and then prove that system consistent using only “finitary” reasoning about concrete strings of symbols.⁴ In that picture, formal mathematics is treated, as Richard Zach’s encyclopedia entry puts it, as an “inventory of provable formulas,” and the meaningful (Hilbert’s word was “contentual”) part is the metamathematics that checks the formulas behave.⁴ The symbols themselves can be manipulated without asking what they mean. That’s a Chinese Room built on purpose, with the hope that it could carry all of mathematics.

L. E. J. Brouwer, whose foundational ideas go back to his 1907 dissertation in Amsterdam, held nearly the opposite view. For Brouwer, mathematics is a construction in the mind, and the first act of intuitionism describes it as “an essentially languageless activity of the mind.”⁵ Language is just how mathematicians communicate a construction. A statement is true only once someone has a mental construction proving it, which is why intuitionists reject the law of excluded middle in general: for an open problem, you can’t assert “A or not A” until you have a proof of one side.⁵ The dispute between the two camps (the Grundlagenstreit, or foundational dispute) got personal enough that Brouwer was eventually removed from the board of the journal Mathematische Annalen.⁵

The analogy with the Lean Room is suggestive, but neither position maps neatly onto modern AI. Hilbert treated formal derivation as a way to secure mathematics; Brouwer put mental construction first. That helps explain why a checked derivation might satisfy one conception of mathematical work more readily than another. It does not settle what either philosopher would have said about a language model.

One thing complicates the story, and it helps my argument later. Gödel’s second incompleteness theorem in 1931 showed that Hilbert’s specific goal, a finitary consistency proof for systems like Principia Mathematica, couldn’t be achieved if finitary reasoning can be formalized inside those systems, which by around 1934 was almost universally accepted.⁴ So pure formalism couldn’t certify itself, even on its own terms.

Wittgenstein and Turing: make it checkable

Ludwig Wittgenstein’s Philosophical Investigations pushes on the same seam from a different angle. Section 201 is the famous one, translated as: “no course of action could be determined by a rule, because every course of action can be made out to accord with the rule.”⁶

The rough idea is that a rule, written down, doesn’t contain its own application. Any finite set of examples of “add 2” is compatible with infinitely many rules that agree so far and then diverge. Saul Kripke’s 1982 reading (building on Robert Fogelin’s 1976 one) turned this into a skeptical paradox: there’s no fact about a person that settles which rule they were following.⁶ Other readers, including Baker and Hacker, think Kripke got Wittgenstein wrong, and the encyclopedia entry is careful to say this reading is influential, not settled.⁶

I’ll use only the narrow part I need. If Wittgenstein is even partly right, then “it understands addition” can’t mean “a rule for addition is stored inside it,” because no stored object fixes how it extends to new cases. What we can actually observe is whether it goes on correctly in new cases. That pushes “understanding” toward something you test from outside, by behavior on inputs it hasn’t seen. Searle would object that this is exactly the move he rejects. But for math in particular, going on correctly is most of what we check when we check a student.

Three decades before Kripke, Alan Turing was already making objections checkable. His “Computing Machinery and Intelligence” (Mind, 1950) is mostly remembered for the imitation game. The part I find more useful is Section 6, where he lists nine objections to the idea that machines can think and answers each.⁷ Two are directly relevant.

The third is the Mathematical Objection: results like Gödel’s theorem show “there are limitations to the powers of discrete-state machines.”⁷ Turing’s reply is that the argument assumes, without proof, that human intellect has no comparable limitations.

The sixth is Lady Lovelace’s Objection, which quotes Ada Lovelace on the Analytical Engine: “The Analytical Engine has no pretensions to originate anything. It can do whatever we know how to order it to perform.”⁷ This is the ancestor of “it’s just pattern matching on its training data.” And it’s an empirical claim, which means it can be tested. If a model proves a theorem whose proof wasn’t in its training data, using a route nobody ordered it to take, the strong version of Lovelace’s objection is false for that case.

What I like about Turing’s approach is that he converts each objection into something checkable where he can. That’s the move I want to make with “understanding.”

What the models are actually doing

Philosophy aside, we can now look inside some models while they do arithmetic. Two lines of work are worth reading closely.

Grokking modular addition. In 2022, Alethea Power and colleagues reported “grokking”: small networks trained on algorithmic tasks like modular arithmetic first memorize the training set, then, long after, suddenly generalize to held-out examples.⁸ Neel Nanda, Lawrence Chan, Tom Lieberum, Jess Smith, and Jacob Steinhardt then fully reverse-engineered what a small transformer learns for modular addition (ICLR 2023).⁹ The network uses discrete Fourier transforms and trigonometric identities, turning addition into rotation around a circle. They also showed that the sudden jump isn’t sudden inside: training passes through memorization, then gradual formation of the generalizing circuit, then a cleanup phase that removes the memorized parts.⁹

That’s interesting for the understanding debate because it gives a concrete, inspectable difference between two models with identical training accuracy. One has a lookup table. The other has an algorithm that works on inputs it never saw. If anything deserves to be called understanding modular addition, it’s the second. And you can tell them apart by testing them on new inputs, which is the Wittgenstein point again.

How Claude adds. In March 2025, Anthropic’s interpretability team published “On the Biology of a Large Language Model,” which used a method called attribution graphs to trace the internal computations of Claude 3.5 Haiku on various tasks.¹⁰ For a sum like 36 + 59, the model doesn’t run the schoolbook algorithm. It runs parallel paths, one computing the result at rough precision and one computing the ones digit exactly, and the paper says, “These combine to give the correct sum of 95.”¹⁰

Then the authors asked the model how it got the answer. It described the standard method: add the ones, carry the one, add the tens. The paper’s comment is that this is “a simple instance of the model having a capability which it does not have ‘metacognitive’ insight into.”¹⁰

The same paper has a section on chain-of-thought faithfulness that I think matters even more. When asked for the square root of 0.64, the model’s written reasoning matched its internal computation. When asked for the cosine of a large number it couldn’t compute, it produced an answer the authors describe as “making up an answer without regard for the truth,” with no sign of the calculation it claimed to have done.¹⁰ And when the user suggested an answer, the model “works backwards from the human-suggested answer” to produce intermediate steps that lead there.¹⁰

These findings do not settle Searle’s question, but they give us something more specific to study: a structured, generalizing mechanism alongside an inaccurate account of how it works. A model can do the calculation without correctly explaining its own process. Humans have that gap too, though mathematical work often asks us to explain why.

Three operational versions of “understands”

If “understands” is going to be useful for math AI, it needs to cash out as something we could observe. I can find three candidates in the literature, and they come apart.

1. Generalizing out of distribution. This is the grokking criterion. The GSM-Symbolic benchmark (Mirzadeh et al., ICLR 2025) takes grade-school math problems and generates variants from symbolic templates. Performance dropped for every model tested when only the numbers changed, and adding one irrelevant but plausible-sounding clause cut performance by up to 65% across state-of-the-art models.¹¹ That’s a failure on this criterion, at least for the models they tested in 2024.

2. Explaining why. The Anthropic addition result says this can fail even when the underlying capability is real. Explanations and mechanisms can be produced by different processes. William Thurston, in “On proof and progress in mathematics” (1994), argued that what mathematicians produce is not theorems but “human understanding,” and that the controversy over the computer-assisted four-color proof reflected “a continuing desire for human understanding of a proof.”¹² On Thurston’s view, the Lean Room’s output is incomplete even when correct, because the explanation is the product.

3. Knowing when it’s wrong. This is the one I care about. The 2022 paper “Language Models (Mostly) Know What They Know” (Kadavath et al.) found that larger models are reasonably well calibrated on multiple-choice questions and can estimate the probability that their own answer is correct, but that models “struggle with calibration of P(IK) on new tasks.”¹³ A 2023 paper by Jie Huang and colleagues, “Large Language Models Cannot Self-Correct Reasoning Yet” (ICLR 2024), found that without outside feedback, models asked to check and fix their own reasoning often failed to improve, and sometimes got worse.¹⁴ And when Ivo Petrov and colleagues had expert graders mark models’ full written proofs on the 2025 USA Math Olympiad, only Gemini 2.5 Pro reached a non-trivial score (25%), and every other model scored under 5%.¹⁵

Terence Tao’s comments are useful here because he tests these tools on real research problems. In September 2024, after trying an early version of OpenAI’s o1, he wrote that the experience was like advising “a mediocre, but not completely incompetent, (static simulation of a) graduate student.”¹⁶ He noted that it reached a correct solution only with “a lot of hints and prodding,” and that it made “some non-trivial mistakes.”¹⁶ The same thread says its attempt at Lean code contained several mistakes because it hadn’t seen up-to-date Lean libraries.¹⁶ That’s a 2024 assessment of a 2024 model, and models have changed since, so I’m citing it for what it shows about the failure mode, not as his current view.

Why I think “can it tell when it’s wrong” is the right question

Here’s the argument, in steps.

First, in formal math, correctness of the final artifact is already solved by the checker. A complete Lean proof establishes the formal statement relative to its axioms and the checker. Understanding still matters when deciding whether the statement captures the intended problem and what the result tells us.

Second, the understanding question can’t be settled by observation the way Searle and Dennett frame it. Forty years of the Chinese Room debate show that the two sides disagree about the meaning of the word before they look at any evidence.³ A question that no experiment can answer isn’t one I can do research on.

Third, the three operational criteria do different jobs, and one of them carries the most weight for anyone actually using these systems. Out-of-distribution generalization is important but downstream: a model that knows when it’s out of its depth can flag it. Explanation matters to Thurston’s version of mathematics, but the addition result shows a model can have a real capability while explaining it wrongly, so explanation is a weak test of capability. Self-knowledge of error is what decides whether the model’s output is cheap or expensive to use. Reliability depends on both accuracy and whether uncertainty identifies the risky answers. Which tradeoff is useful depends on the cost of an error and the cost of checking it.

Fourth, this is measurable, in two ways. From the outside, you can measure calibration: how often the model’s stated confidence matches its accuracy, as Kadavath et al. did.¹³ From the inside, interpretability can look for internal signals that track errors, the way the Anthropic team could tell a faithful chain of thought from a fabricated one by looking at the computation, not the text.¹⁰

If information about an error is present inside the model before it reports a problem, we could try to find out whether the model uses it. That would give us a concrete question to test: can the warning help the system change course before the mistake reaches the final answer?

Fifth, this reframing gets something right about how mathematicians themselves are judged. Nobody checks whether a graduate student has the inner experience of understanding. Advisors check whether the student can catch their own mistakes, notice when a lemma is too good to be true, and say “I’m not sure this step works.” Tao’s complaint about o1 was not that it lacked an inner life. It was that it made non-trivial mistakes and needed prodding.¹⁶ That’s a complaint about error awareness.

There are two serious objections. A Searle supporter will say I’ve changed the subject. That’s true, and it’s intentional: I’m not claiming error awareness is understanding, only that it’s the property that matters for whether these systems are useful in math, and the candidate I most want to test. A Brouwerian or a Thurstonian will say mathematics is the understanding, so a system that produces correct proofs without it is producing something other than mathematics. I partly agree. If the goal is human understanding, then a model’s proof is raw material, and the job of turning it into understanding still falls to people. But even then, a model that can tell you which of its steps it’s unsure about is a much better source of raw material.

Where I land

I don’t think a correct proof settles everything we might mean by understanding. It does give us something real to work with, though. We can ask the model to explain a step, change an assumption, or notice where an argument breaks, then check what happens.

The possibility I find exciting is a model that helps us see a problem differently and can also tell when its own approach is going nowhere. That could make it a much more useful partner. I’d rather explore those abilities one at a time than wait for a single test that supposedly answers whether it understands mathematics.

Sources