A Proof Doesn't Know Who Wrote It

Key Takeaways

• A poster on r/askphilosophy, persuaded by Searle and Dreyfus that AI does no thinking, asked what it means that AI now solves math problems at something like Fields Medal level. Either the machines think, or hard mathematics needs no thinking, and both feel wrong.
• The dilemma rests on merging two different skeptics. Dreyfus made capability predictions, which results can refute, and one of his fell to a chess program in 1967. Searle’s Chinese Room stipulates perfect output and argues it still would not be understanding. No theorem, however deep, touches that argument.
• What happened is also less uniform than “AI solves math”: an officially graded Olympiad gold, an AI-suggested construction proved by humans, ten machine-generated proofs shipped with Lean certificates, and one celebrated claim that turned out to be a literature search.
• A proof is the rare artifact whose validity can be checked without knowing where it came from. Mathematics is therefore the domain least dependent on trusting the producer, which is exactly why it fell first.
• The mathematicians closest to the event are not asking whether the machine thinks. The Leiden Declaration and Tao’s ICM essay both ask a different question: what is mathematical research for, once producing true statements is no longer scarce?

Someone on r/askphilosophy recently asked a question that deserves a longer answer than a comment thread allows. Their position, shaped by reading Searle and Dreyfus, was that AI systems do not think at all. But AI is now, in their words, basically solving math problems at Fields Medal level, and the obvious escape route, concluding that you do not need any reasoning to solve them, sounded wrong to them too. They asked whether this is a rerun of the unease that followed Deep Blue’s win over Kasparov.

It is a genuine dilemma, honestly stated: either the machines think, or the hardest problems we know of can be solved without thinking. Each horn gores something the asker believes.

What Actually Happened?

“AI solves Fields Medal math” compresses at least four events with very different anatomies, and the meaning of each depends on its anatomy. The one substantive answer the thread received made this point through a famous machine-learning parable: a skin-cancer classifier that matched dermatologists until someone looked closer and found it was largely detecting the rulers dermatologists place next to malignant lesions. Before asking what a result means, establish what the system actually did.

So, the record. In July 2025, Google DeepMind’s Gemini Deep Think earned 35 of 42 points at the International Mathematical Olympiad, solving five of six problems, with solutions graded by IMO coordinators under the same criteria applied to students. A real milestone, but competition mathematics: problems designed to be solvable by brilliant teenagers in hours, which is a different activity from research.

In October 2025 came the cautionary entry. An OpenAI vice president announced that GPT-5 had found solutions to ten unsolved Erdős problems. The maintainer of the Erdős problems database, Thomas Bloom, called the announcement a dramatic misrepresentation: “open” on his site meant open so far as he knew, and the model had located existing solutions in published literature. The post was deleted; Demis Hassabis called the episode embarrassing. The model had done something genuinely useful, an expert literature search, that was announced as something else entirely.

Then 2026. In late July, the 150-year-old Maxwell Conjecture fell to a five-charge counterexample whose key geometric construction was suggested by GPT-5.6 Sol, with the proof done entirely by three human mathematicians. I wrote about what that division of labor does and does not mean at the time: the model proposed a direction, and humans made it mathematics.

And on August 1, OpenAI published ten results on long-standing open problems, from sphere-packing bounds to a construction establishing the existence of non-sofic groups, attributed to an internal version of Astra, its next major model. This is the strongest version of the claim so far, and its details deserve attention. OpenAI states that “the mathematical arguments themselves were generated by our system,” that humans prepared the manuscripts, and that the model formalized each argument in a Lean certificate: a machine-checkable version of the proof. The company also reports that finding the solutions cost roughly two thousand dollars of compute at current API rates, a number that will do quiet work in a moment.

Four events, four anatomies: graded competition performance, a misread literature search, a suggested construction proved by humans, and machine-generated arguments with formal certificates. Anyone arguing about what “it” means should first say which of these they mean.

Does Producing a Proof Refute Searle?

Now the philosophy, because this is where the dilemma comes apart.

The asker cites Searle and Dreyfus as one position, and for the purposes of this question they could not be more different. Dreyfus made capability claims: his 1965 RAND paper “Alchemy and Artificial Intelligence” argued that the cognitive assumptions underlying AI research were philosophically untenable, and he noted that a chess program had lost to a ten-year-old. Capability claims are refutable by capability, and this one was: in 1967, Richard Greenblatt’s MacHack VI checkmated Dreyfus himself in a match MIT arranged for the occasion. Dreyfus’s deeper arguments about embodied skill were not settled by that game, but the falsifiable perimeter of his position fell where it was falsifiable.

Searle built his argument so that no such perimeter exists. The Chinese Room, from his 1980 paper “Minds, Brains, and Programs,” begins by granting everything about performance: the person in the room, following the program, produces answers good enough that those outside are convinced they are corresponding with a native Chinese speaker. The argument’s entire point is that even this, output as good as output gets, would not constitute understanding, because manipulating symbols by rule, in Searle’s slogan, is not sufficient for semantics. You can reject the argument on many grounds, and much of the philosophy of mind has spent four decades doing so. But you cannot refute it with a theorem. A stipulation of perfect performance is not threatened by instances of perfect performance.

This is why the asker’s dilemma has no bite against Searle. “AI solves Fields-level problems, therefore either it thinks or the problems need no thinking” borrows its force from the assumption that solving is evidence of thinking. Searle’s argument exists precisely to sever that inference. If he is right, machines can in principle do everything and understand nothing, and mathematics was never going to be the exception. If he is wrong, it will not be a theorem that shows it.

Then Does Mathematics Not Require Reasoning?

The second horn is the one that “sounds wrong,” and it should, because it equivocates on “reasoning.”

There is reasoning as a property of an artifact: a proof is a chain of inferences, each step checkable by a referee, and now by software, without any reference to what produced it. And there is thinking as a property of a producer: the felt activity of understanding, the having of the question rather than the answering of it. The dilemma collapses these. The proofs of 2026 contain reasoning in the first sense no matter what generated them; the Lean certificates make that checkable by machine. Whether anything thought, in the second sense, is untouched either way.

Mathematics is the domain where this separation is cleanest, and that is not incidental to why it fell first. A medical diagnosis, a legal argument, an engineering signoff: each of these leans, in the end, on trusting the judgment that produced it. A proof does not. It is the rare artifact that carries its own justification, and the discipline has spent a century and a half making that literal, from formal logic to proof assistants. The result is that mathematics can accept an artifact from a producer it does not trust, because the checking never depended on trust in the first place.

We know this because mathematics already ran the experiment, with the roles reversed. In 1976, Appel and Haken proved the four color theorem using over a thousand hours of computer time to check 1,834 configurations that no human could survey. The philosopher Thomas Tymoczko argued in 1979 that accepting it meant changing what “proof” means: mathematicians were now accepting a result partly on the testimony of a machine process no one could hold in their head. The controversy was real and slow to die, and it ended undramatically: in 2005 Gonthier and Werner formalized the entire proof in the Coq proof assistant, removing the need to trust the original ad hoc programs at all. Fifty years ago the machine did the checking and humans supplied the idea, and mathematics renegotiated its standards rather than abandon the theorem. Now the machine supplies the idea and the certificate, and humans decide what the theorem is worth. The negotiation is the constant; only the seats change.

Is This Deep Blue Again?

The asker’s own analogy is the right one, and its aftermath is the best available guide.

In May 1997, Deep Blue beat Garry Kasparov 3.5 to 2.5 in New York. Two conclusions were on offer, and the interesting fact is that the chess and AI communities declined both. Almost nobody concluded that Deep Blue thought; almost nobody concluded that chess had never required intelligence. What actually changed was the status of the task: chess quietly lost its two-century role as a proxy for thought. The capability event turned out to be a discovery about chess, that world-class play is reachable by search at sufficient scale, not a discovery about minds.

Mathematical problem-solving is now undergoing the same reclassification, and OpenAI’s two-thousand-dollar figure is the tell. A price tag on solutions to decades-old open problems is the clearest possible statement that theorem-production is becoming an industrial process rather than a proxy for genius. When a task stops being scarce, it stops being usable as evidence of the thing that used to make it scarce. That is what happened to chess in 1997 and to Go in 2016, and it is what “Fields Medal level” is undergoing now.

But the analogy also has a limit worth respecting. A chess win is terminal: the game ends, the pieces are reset, nothing downstream depends on the winning move meaning anything. A theorem is not terminal. It feeds the next conjecture, reorganizes a field’s sense of what matters, teaches the people who understand its proof how to see. Chess could afford to lose its proxy status and carry on as sport. Mathematics losing its proxy status forces the harder question of what, exactly, the residual human activity is. Which is why the most serious responses to 2026 are not about machines at all.

What Do the Mathematicians Say It Means?

The people with the most at stake have conspicuously not framed this as a debate about machine minds.

In June 2026, after a working group that began at a Lorentz Center conference the previous autumn, the Leiden Declaration on Artificial Intelligence and Mathematics was published with the International Mathematical Union’s endorsement and thousands of signatories, Terence Tao and Peter Scholze among them. Its worries are all epistemic and institutional, not metaphysical: automated techniques “can produce plausible but unreliable (or even incorrect) arguments which are difficult to distinguish from correct mathematical proofs”; outputs that fail to cite the human work they synthesize; incentives that reward AI use for its own sake; results announced “through press releases or blog posts” rather than peer review; and the risk that “research questions may come to be prioritized because of their amenability to automated mathematics, rather than expert judgment.” Every one of these is a worry about how a community knows things and rewards people. None of them requires an answer to the Chinese Room.

Tao went further. His essay for the 2026 International Congress of Mathematicians, “Mathematics in the age of AI”, performs the exact move this question needs, stated in its abstract: “Rather than debating the capabilities of such tools, we condition on the hypothesis that these capabilities will arrive, and examine instead a question that is orthogonal to it: what the goals and values of mathematical research actually are.” Condition on the capability. Ask about the values. Tao, himself a Fields Medalist, looked at the arrival of machine theorem-proving and concluded that the urgent question is not what the machine is, but what mathematics is for.

Notice what this response presupposes. If mathematics were only a theorem-production industry, the Leiden signatories would be negotiating severance, not standards. The reason the values question is live is that producing true statements was never the whole activity. Mathematicians prove things in order to understand them, to teach them, to see what the proof reveals about neighboring problems. Understanding is the part of the activity Searle said the room lacks, and it is precisely the part the community is now organizing to preserve, the part that asks the next question rather than answering the current one.

So What Is the Meaning?

Three things, one per level.

About machines: almost nothing. The results refute capability skepticism, Dreyfus-style, about this class of task, as thoroughly as MacHack refuted it about chess. They neither refute nor support Searle, whose argument granted arbitrary capability before the first transformer was trained. Anyone announcing that the theorems prove machines think, or that machines still cannot really think, is reading their prior off the scoreboard.

About mathematics: something real and slightly deflationary. Research-level theorem-proving joins chess and Go in the class of tasks achievable without whatever it is humans have. The asker felt that “you don’t need reasoning to solve them” sounds wrong, and the resolution is that you don’t need a reasoner: the reasoning is in the artifact, checkable by a kernel that understands nothing, purchasable at API rates. Mathematics is not diminished by this any more than it was diminished in 1976. It is, once again, renegotiating what it accepts and what it is for.

About us: the Deep Blue lesson, one level up. The meaning of a capability event is mostly the reclassification it forces. Chess taught us that a task can lose its status as a proxy for thought while everything we actually valued about the task, the beauty, the pedagogy, the human contest, survives intact. Kasparov kept playing, and chess kept being worth playing. What has to be given up is only the use of the task as a mirror. The question the r/askphilosophy poster asked, what does it mean, is the reflex of looking into that mirror one more time and finding it occupied. Tao’s answer, and the honest one, is to stop asking what the occupant is and start asking, with the mirror gone, what we were looking for in it.

That question, unlike the Maxwell Conjecture, does not come with a certificate. The thread that runs through these essays on AI in science and mathematics is that where a machine’s contribution ends and a human’s begins is a boundary that has to be redrawn case by case, and the redrawing is not optional. A proof doesn’t know who wrote it. We are the ones who have to know, and say, why we wanted it written.

Further Reading

• Tao, T. (2026). “Mathematics in the age of AI.” arXiv:2608.16753. The ICM essay: condition on capability, ask about values.
• The Leiden Declaration on Artificial Intelligence and Mathematics (June 2026). The community’s own statement of what is actually at risk.
• OpenAI (2026). “Ten advances in mathematics and theoretical computer science.” The strongest current claim, with Lean certificates on GitHub.
• Searle, J. (1980). “Minds, Brains, and Programs.” Behavioral and Brain Sciences 3(3). See the Stanford Encyclopedia entry. The argument the results cannot touch, by design.
• Tymoczko, T. (1979). “The Four-Color Problem and Its Philosophical Significance.” Journal of Philosophy 76(2), 57-83. Mathematics renegotiating proof the first time.
• Arathoon, P., Ball, G., Kvalheim, M. D. (2026). “The Maxwell Conjecture is False.” arXiv:2607.27197. The suggestion-plus-human-proof anatomy, examined in an earlier essay here.

More essays at Call to Think · About this project