On 1 June 2026, New Scientist published Alex Wilkins' account of attempting a problem that had defeated trained mathematicians. He has no mathematical training beyond an undergraduate physics degree. He fed an open Erdős problem, number 710, into GPT 5.5 Pro and waited. After 22 minutes and 18 seconds the model returned what it called a clean proof. He fed it back; the model confirmed the main argument was correct. For a few minutes he believed he had solved a decades-old problem.
He had not. When he sent it to Kevin Barreto, the Cambridge undergraduate who has cracked several Erdős problems with AI, the verdict came back fast: it doesn't solve the problem. The model had proved something adjacent, a formula Erdős himself had already settled years earlier. A working mathematician would have caught it on sight. Wilkins, lacking the training, could not. The output was internally valid and aimed at the wrong target.
Hold that detail. It is the whole story.
Start with the record, because it is real and I am not going to soften it.
In July 2024, Google DeepMind's AlphaProof reached a silver-medal standard on that year's International Mathematical Olympiad. A year later, Google reported officially graded gold-level performance with Gemini Deep Think, while OpenAI reported a separate gold-level result with a general-purpose reasoning model. In January 2026, Jim Bryan, Balazs Elek, Freddie Manners, George Salafatinos and Ravi Vakil posted an algebraic-geometry and algebraic-topology result obtained in conjunction with Google Gemini; the same month, Tony Feng and collaborators described Aletheia computing eigenweights in arithmetic geometry, with the mathematical content machine-generated. Thomas Bloom, who runs the public Erdős-problem tracker, has verified AI-assisted solutions that he says took non-trivial effort.
And the headline result is not only real, it is bigger than the casual framing suggests. New Scientist describes an internal OpenAI model being used in May to "solve" the planar unit distance problem, posed by Erdős in 1946. The word solve undersells what happened, and the precise version is the one worth stating: on 20 May 2026, OpenAI announced that the model had disproved the long-held assumption that square-grid arrangements were essentially optimal, finding an infinite family of configurations that beat them, an improvement later quantified by Princeton's Will Sawin at an exponent of roughly 0.014. Fields medallist Tim Gowers and Sawin both verified the proof.
These are not parlour tricks. Theorems moved. The proofs check out. Anyone who tells you otherwise is selling comfort.
So this is not an argument that the machines failed. It is an argument that we are reaching for the wrong word. We keep saying understand. What is documented is generate. Everything below is my case for why that distinction is the one that matters.
Look at how the wins were produced, because the method gives the game away.
The Vakil paper is explicit about the human role: the question, framing and final exposition came from human authors, even though a key proof step came from Gemini. Barreto describes coaxing a proof from the model as essentially playing the lottery, and says the trick is to hint that the problem is easier than it is, to tell the model to try and not give up. Wilkins copied that technique. You do not encourage a colleague who reasons. You tune a sampler that searches.
This is the same architectural thesis I argued in The Faster Idiot Paradox, carried into number theory, and I'll put the strongest evidence for it on the table rather than assume it. The Epic sepsis model scored well in deployment until independent researchers restricted its inputs to data recorded before a clinician acted, at which point its discriminative ability fell to roughly a coin flip. It had learned to detect the physician's suspicion, not the disease. That is documented fact, published in NEJM AI in 2024. The analogy to a language model proving a theorem is mine, and you should judge it as one: the system has absorbed the published corpus and samples plausible continuations from it. When the sample is a valid chain, we call it insight; when it solves the wrong problem, as it did for Wilkins, we call it error. Both come from one process, and the model cannot tell them apart. That is why a human still has to.
It is not that AI proves theorems. It is that AI generates candidate proofs that humans must still verify, from problems that humans must still choose.
I owe the other side its best shot, and there are two. The first is empirical, the second goes to the root.
The empirical one is Von Mangoldt. When Liam Price elicited a solution to Erdős 1196 from a single request to ChatGPT 5.5 Pro, the model reached for the Von Mangoldt function, a tool prior human attempts had missed. Jared Lichtman, who had spent part of his PhD nearby, confirmed it circumvented difficulties earlier approaches had snagged on, and his group later adapted the technique to crack a related sixty-year-old conjecture. This genuinely looks like the machine seeing what we couldn't.
I read it as coverage, not depth. A human number theorist lives inside one subfield; the model holds all of them and can retrieve a tool sitting one field over that no individual had loaded. That is a real and valuable capability, and it is also exactly what a statistical system trained on everything would produce, so it does not by itself distinguish search from understanding. The reason I lean to search is the same anecdote's other half: the model that found Von Mangoldt for Price is the model that handed Wilkins a confident proof of the wrong theorem. I'll come back to why that pairing is decisive, because it is.
The second objection is the one that can actually kill this essay, so let me state it at full strength. It runs: your whole argument rests on generate and understand being different things, but you never say what understanding is. If you can't name an operation a comprehending agent performs that a searching one can't, then "understanding" is just an honorific you pin on systems you like. And here is the sharp end: a brain is also pattern-matching, only wet. When you grasp why a proof holds, you are running learned recognition of valid inference chains. The difference between you and the model is degree, not kind. Scale the search over a rich enough representation and you don't approach understanding, you arrive at it, because there was never an extra ingredient. If that is right, the machines already understand, my distinction is a word, and the architecture I am about to propose solves a problem that doesn't exist.
That objection deserves a real answer, not a bow. Here is mine, and it is falsifiable, which is the only kind worth giving.
Stop defending understanding as a property and define it as a measurable capability: intervention. A searching agent predicts what correlates in the distribution it learned. A comprehending agent predicts what happens when you break the pattern, counterfactually, under conditions it has never seen. That is not philosophy; it is Judea Pearl's do-operator, and it predates this fight by twenty-five years. Now watch what it does to both objections at once.
It resolves Wilkins. The model could not tell a valid proof from one that solved the wrong problem, because both looked the same inside the distribution it had absorbed. It had no operation for intervening on the argument and checking what actually follows, so it returned plausibility and called it proof. A system that tested consequence would have caught the mismatch. Search cannot, because search has no outside-the-distribution to test against. The Von Mangoldt win and the Wilkins failure are not two phenomena. They are one mechanism, sampling plausible continuations, succeeding and failing with identical serenity. That identical serenity is the signature of search. Understanding is not serene when it is wrong.
And it answers the brain objection on its own terms. Grant that a brain pattern-matches. The claim that the difference is only degree is itself an empirical claim, and it is false in the place that matters: generalisation. A searcher trained on everything fails systematically outside its distribution; a causal model transfers to cases it has never seen, sometimes from a single observation, the way a child learns that pushing a glass off a table breaks it without needing ten thousand glasses. That is not more of the same curve. It is a different curve. The gap between degree and kind is not rhetorical here, it is the gap between interpolation and extrapolation, and it shows up in measurements, not in definitions.
So the honest position is not that machines can't understand. It is that understanding is the capacity to predict under intervention, search is the capacity to predict under repetition, and the current systems demonstrably do the second. That is a line you can attack. Build a pure searcher that generalises counterfactually, out of distribution, as well as a causal model does, and I am wrong, the boundary was an illusion, and everything I propose below is wasted. I don't think you can. I have spent years trying to build the thing that does the other. But that experiment, not my conviction, is what settles it.
Terence Tao and others have framed the shift as proof scarcity giving way to proof abundance: if candidate proofs become cheap, the bottleneck moves toward verification, explanation and understanding. I accept that framing and extend it: if proofs are abundant, then producing them was never the scarce resource. Knowing which are worth having, and why they hold under intervention, was. That part has not moved.
In the new mathematics a human chooses the problem, reduces it to a form the model can sample against, coaches the prompt through the failed attempts Barreto described, verifies the output as Barreto did for Wilkins, and decides whether the result matters, which is Melanie Wood's question of whether a solution opens roads or closes one. Daniel Litt stated the limit plainly: a model cannot do your understanding for you.
I drew the same map in The Wizard of Silicon Valley, about a different magic act with the same hidden machinery. Strip those four human functions out and what remains is not an AI mathematician. It is a proof-shaped slot machine. Tsimerman ran the test at the April conference: in a future where you press a button and a proof sometimes drops, who still wants to be a mathematician? About half the room raised a hand. Not because the work vanishes, but because the part they love does, if all that's left is checking tickets.
Now the constructive half, and here I have to be most careful, because this is where it is easiest to sell a vision as if it were a product.
The field's instinct is to scale the generator: bigger model, more maths in the training set, a better sampler. That improves the lottery and does nothing for the three human functions, because those are not generation problems. They are understanding problems. Here are three layers that address them, sorted honestly by how real they are today.
A falsification engine. This one exists. A generator must never be its own judge, and the model telling Wilkins his proof was correct is that failure in miniature. The fix is mature technology: pipe every candidate into a formal verifier, Lean or an equivalent, so correct means machine-checked against axioms rather than plausible to the model that wrote it. DeepMind's AlphaProof already formalises its reasoning in Lean. This is not a proposal, it is an available engineering choice, and the scandal is that the consumer models people are using to attack Erdős problems mostly don't make it, which is precisely why a physics graduate could believe he'd made history for ten minutes.
A significance layer. This is a proposal, not a system. Validity is now cheap; significance, whether a result unlocks others, is the scarce judgement, and it lives in how a theorem connects to the field's web of dependencies. I claim that structure is buildable, that a system holding the dependency graph of known mathematics could estimate whether a candidate is a dead end or a hub. I am not aware of a deployed system that does this, and buildable is my argument, not a demonstration. It doesn't ship today partly because it doesn't demo as a clean rising line on a benchmark. I think it is the more valuable engine anyway. You are entitled to treat that as an unproven bet.
A causal memory of why. This is the part I've spent years on, and I'll stake it openly rather than smuggle it. A system that stores not proofs but the causal structure of why a proof works could transfer a technique, the Von Mangoldt move, to a new problem on its own, instead of waiting for four humans to spot the analogy. I have built systems on this principle and made specific, falsifiable performance claims about them in The Faster Idiot Paradox, including head-to-head benchmark results and real-time autonomous decision counts. I am not going to repeat those numbers here as if this essay verified them, because it doesn't. They are my claims, published under my name, made falsifiable on purpose. The correct response to a falsifiable claim is not to trust it. It is to test it. That invitation is the most honest thing I can offer, and it is also the whole point of building this way.
None of these three is more compute. Together they are a different machine.
What follows is advocacy, not forecast. I think one future is better and I am trying to talk us into building it. Read it as that.
There is, on the documented evidence, no AI mathematician yet. There is a magnificent generator and a human who chooses, checks, and interprets. Calling the pair an AI mathematician is a marketing decision, and it points us at the wrong mountain. Name it correctly and the path clears: we have automated the production of proofs and barely touched the understanding of them. So the work is to build the understanding. That is a larger ambition than adding zeros, not a smaller one.
And the prize, if Tao's abundance is real, is genuine. For the whole history of the discipline the rate limit was the cost of one correct proof, years of a life per theorem. If that constraint is falling, a field whose bottleneck shifts from production to judgement is not running out of room; its ceiling is coming off. Kontorovich has already described projects he can now imagine starting because the cost of proof exploration has changed. That is one mathematician's optimism, not a measured trend. But if it generalises, it points at the steepest expansion of human reach since the calculus, with the human lifted to the one seat that was always scarce: deciding which mountains are worth climbing.
That is the version I am building toward, and it rests on bets, the significance layer unproven, the abundance early, my own architecture a claim I have put my name to and asked you to test. What I will not pretend is that it is inevitable. Scale the lottery and you get a faster slot machine and a generation of mathematicians checking tickets. Build the missing half and you get a partnership: a machine that can be made to understand consequence, working under a human who decides what is worth understanding. One of those arrives by default. The other we have to choose, and choose soon, because what we build in mathematics, where a wrong answer is simply wrong and no consensus can save it, is what we will build everywhere else, in medicine, in the systems that drive our cars and price our risk and sort our children.
The field thinks it is running out of places to hide. It has it backwards. The asking, the judging, the knowing-why, none of that has been automated, and the machines that look like they are closing the frontier have freed the one human faculty that opens it.
A proof can tell you that something is true. It was never able to tell you why it mattered, or what to ask next. Give the machine the first. Keep the other two. Build the bridge between them, and prove me right by testing every claim I just made. That is not the end of mathematics. It is the discipline finally getting honest about which part was ever the hard one.
Claim ledger
What is asserted here.
The Wilkins account is sourced to New Scientist; the unit-distance disproof to OpenAI; the IMO milestones to Google DeepMind; the sepsis example to NEJM AI DOI 10.1056/AIoa2300032.
The distinction between proof generation and mathematical understanding is the essay's argument, not a claim made by the cited labs.
The falsification, significance and causal-memory layers are presented as architecture choices to test, not as already accepted field standards.