What do we actually lose when a machine gets the answer right for reasons nobody can follow?
The Margin
In 1637, Pierre de Fermat wrote a note in the margin of a book: he had found a truly remarkable proof of a theorem about whole numbers, but, as he put it, "the margin was too narrow to contain it."
"Hanc marginis exiguitas non caperet."
He never wrote it down anywhere else. Mathematicians spent the next 358 years unable to decide whether he was right, wrong—or simply out of paper. Andrew Wiles finally closed it in 1995, after seven years of secret work, with one of the landmark proofs in the history of mathematics—well over a hundred pages, using mathematical machinery Fermat could never have had access to.
Thirteen Million Lines
A few days ago, a small Anthropic team led by researcher Tianyi Peng tasked a swarm of Claude agents with processing this proof: not to write a new one, but to translate the monumental work of Wiles into Lean, the same language used to verify software code as well as to formalize a mathematical proof. The first attempts apparently failed in a specific, telling way: the agents themselves drowned in the complexity of the abstraction, losing track of the project's state and dropping out of collaboration, each one rediscovering or contradicting what the others had already done.
The fix was structure rather than a better model. Prove2Me, the platform they ran it on, keeps a DAG—a directed acyclic graph—of every theorem statement still needed, letting the proof's structure emerge from the depths instead of staying trapped inside any single agent's head. Not only was the proof too long to fit in the margin of Pierre de Fermat's notebook—apparently, it was also too long to fit inside the head of a many-trillion-parameter agent.
Hanc marginis exiguitas non caperet.
Eleven days later the proof finally emerged from the depths: 13 million lines of Lean—more than five times the size of Mathlib, mathematics' largest community library!—over 30,000 intermediate theorems proved and stitched together. Human mathematical input came down to occasionally nudge the agents, closer to a coach barking from the sideline than a mathematician at the blackboard—the same push you'd give Kylian Mbappé to go tackle Lionel Messi: like "push Mazur to be done soon." Anthropic published a fascinating visualization showing the graph blooming outward in three colored zones, each an entire region of mathematics supplying an essential link to the final proof—a keystone holding up its share of a vertiginous cathedral of mathematical abstraction.
Anthropic's dependency graph, blooming outward as the formalization runs.
A short story by Edgar Allan Poe, A Descent into the Maelström (1841), tells how a fisherman dragged into a whirlpool gets out of it: he watches the wreckage circling alongside him long enough to notice that barrels sink more slowly than boats, then ties himself to one and lets his own boat go. 30,000 theorems is chaos by any ordinary definition—and the graph was the barrel. The model produces. The graph gives shape. Lean verifies.
The follow-up matters as much as the result: the same method allegedly formalized Vinogradov's three primes theorem in three days, this time using only consumer Claude Max subscriptions. Eleven days, then three, on hardware anyone can rent.
The Same Safety Net
A month earlier, OpenAI had published ten solutions of its own to mathematical problems untouched for a decade or more—group theory, quantum complexity, a sphere-packing exponent unmoved since 1978—produced by a pre-release version of Astra. Every proof came formalized in Lean too. Cost to find all ten: allegedly around $2,000.
Neither team was asking anyone to trust the model's reasoning. Both were asking people to trust a small, boring verifier instead, and to stop caring whether the path to the answer was legible. That's the actual point of Lean: it doesn't grade the reasoning, only the destination. That certificate is indisputable, and yet what happens inside the model to get there is becoming more of a mystery by the day: mathematical insight, or brute-force search? Anthropic's dependency graph adds something extra on top, almost as a byproduct—not just a certified result, but a full, readable map of how it got built, one theorem at a time. Whether that extra part holds up is a separate question.
Astra finally shipped last week as GPT-6 Astra, and according to the first technical reports, it reasons through an architecture OpenAI calls "recurrent depth": rather than writing its thinking out as tokens anyone can read, it loops its hidden state through the same layers, several passes deep, leaving no written trace of the intermediate steps. OpenAI has acknowledged the tradeoff—the model is harder to monitor than its predecessors—and says improving that remains a research priority. None of this touches whether Astra's answers still hold; Lean still says yes or no either way. It touches something else: whether the road to the answer stays visible to anyone at all.
What We Actually Lose
Mathematicians saw this coming. Published on 2 June, the Leiden Declaration drew 130 signatures on its first day and passed a thousand within twenty-four hours—Terence Tao among them, endorsed by the International Mathematical Union. Most of it argues something concrete and institutional: attribution rarely follows the mathematicians whose proofs trained the model, consent is often absent, access stays unequal.
But one line reaches further than the rest:
"Mathematics produces not only a body of results, but also understanding, clarity, and judgment among the communities of mathematicians who have shaped them."
A Non-Renewable Resource
A month after Leiden, the same Terence Tao made a sharper worry, in an essay for the 2026 International Congress of Mathematicians. His starting distinction: "what is the answer to X?" and "what can be learned from studying X?" used to be practically the same question—reaching an answer meant first understanding why every existing method failed, inventing new tools along the way. AI can now separate them, and in some cases the two become negatively correlated: the faster the machine reaches an answer, the less anyone learns getting there. Solving a hard problem, he writes, used to unfold like a hike into unmapped territory, leaving markers behind as you went. AI can be the helicopter that drops you straight at the summit. You arrive. Nothing gets mapped. You're parachuted onto an island somewhere past the jagged frontier, with no memory of how you got there.
Tao pushes the argument one step further: once a machine has publicly solved an open problem, nobody can go back to not knowing. The problem is contaminated, and it becomes far harder to tell whether any later approach is a genuine rediscovery or just an echo of the known solution. Good open problems, in his account, are starting to look like a non-renewable resource.
Indiscriminate automated strip-mining of open problems for solutions is like using excavators to dig treasures out of an archaeological site.
An excavator recovers the treasure faster than any archaeologist could. It also destroys the stratigraphy that let anyone understand where the treasure came from, or what it meant. Brute-force discovery.
The Second Job
A proof has always done two jobs at once: certify that something is true, and explain why. Lean does the first almost perfectly, and in doing so quietly makes the second optional. Correctness survives that trade intact; the explanation is what goes. Potentially millions of true, certified statements, functionally dead to human understanding.
Mathematics has quietly assumed for twenty-five hundred years that it was written for us, mostly because we were the only ones capable of writing it. That assumption may simply stop holding. Unintelligible and meaningless are not the same thing, and a result nobody can follow is still a result.
Fermat's margin was too small for his proof. A context window is too small for this kind of reasoning. Both times the answer was structure rather than more room. One question left is whether we keep building the kind we can still read.
What do we actually lose when a machine gets the answer right for reasons nobody can follow?
I keep landing on the same one I opened with—recurrent, at whatever depth you read it.
