For twenty-five centuries, mathematics was protected by a simple, comforting equation: if a person wanted to prove a difficult truth about the world, they had to understand it first.
The struggle to find a proof was brutal, slow, and solitary. But the reward was indivisible. The mathematician who crossed the desert of chalk and scratchpads arrived at the summit not only with a verified result, but with an insight: a mental picture of why the universe hung together in that particular way. That picture could then be taught to students, argued over in faculty lounges, and woven into textbooks. Proof and understanding were born together as twins.
In the second week of September 2026, that twinship was violently severed.
An artificial intelligence system developed by OpenAI generated a formal proof for one of the most famous unsolved challenges in science: the two-century-old Navier-Stokes problem, which governs how fluids flow, churn, and break. The system did not arrive at the answer through human intuition; it found it by orchestrating a massive swarm of autonomous reasoning agents running across server racks for days, checking every intermediate step against an automated logical compiler called Lean. (Specifically, OpenAI’s run claimed a finite-time singularity under smooth external forcing, addressing variants (C) and (D) of the Clay Millennium problem for Navier-Stokes; see the OpenAI NavierStokesAndEuler repository on GitHub. This triggered an immediate priority dispute with mathematicians Tristan Buckmaster and Levent Alpöge, who had posted neighboring work that same week.)
The output was mechanically flawless, verified to the absolute bedrock of formal logic. But it arrived as tens of thousands of lines of machine code. No human being had conceived the argument. No human being could read it. And no human being could explain it.
Almost immediately, the mathematical world fractured. Twenty-five Fields medalists, the highest honorees of the discipline, published an urgent declaration warning that the soul of their field was in jeopardy. Famous problems, they protested, were never just puzzles to be cracked; they were "landmarks and lighthouses" meant to foster human comprehension. To turn these lighthouses into marketing benchmarks for corporate AI models was to reduce the highest adventure of human reason to an automated lottery.
From the outside, the reaction was swift and unsympathetic. On Marginal Revolution, the economist Tyler Cowen told the mathematicians that their moral outrage was misplaced. The market does not care about guild traditions, Cowen wrote; if machines can settle theorems and unlock practical applications faster and more reliably than scholars, mathematicians will simply have to adapt, even if it means accepting a lower status as the "subordinates or handmaidens" of AI. Meanwhile, educators like Po-Shen Loh rushed to defend their colleagues by arguing that mathematicians might still find employment as technical supervisors, guarding society against out-of-control software.
I do not write this as a research mathematician; my training is in philosophy, where slow, solitary reading was the entire discipline, and I spend my days now building with systems designed to automate intellectual production. I cannot evaluate the fluid mechanics of the Navier-Stokes equations. But I recognize the shape of the crisis.
Both sides in this debate are missing the real event. The mathematicians are fighting a rearguard battle to defend an artisanal past that cannot be restored; their critics are cheering a mechanical efficiency that cannot comprehend what it has produced.
To explore what this transition asks of us, we can consider three quiet movements:
Where the adjective sits: Looking back to the decade when the word "computer" migrated from human beings to machines, to see where the qualifier "human" is drifting today.
Two-thirds of a solution: Borrowing an economic lesson from the spreadsheet and Terence Tao’s anatomy of proof, to ask why cheap mechanical verification makes human digestion the scarcest craft in the room.
Mourning the assurance: Turning to Stanley Cavell and Henry David Thoreau to ask what it means to mourn an artisanal world with courage, so that we might improvise a shared life beyond its ceremonies.
Where the adjective sits
There is a quieter handover I have examined before, in The Cost of a Question. For three hundred years, as David Alan Grier documented in When Computers Were Human, a "computer" was a person. It was a job title, held by clerks, by the women who catalogued stars at Harvard, by the human calculatrices who drafted the nautical tables that guided ships through fog. When Alan Turing wrote the paper that founded computer science in 1936, the word "computer" in his text referred exclusively to a human being. The machine inherited the name along with the task.
By 1962, when John Glenn was preparing to orbit the Earth in Friendship 7, the handover was far enough along that an electronic mainframe had calculated his flight trajectory. Yet Glenn did not trust the machine alone. As recorded in her NASA biography, he famously told the flight engineers to "get the girl," asking Katherine Johnson to rerun the orbital equations at her desk, by hand. "If she says they’re good," Glenn told them, "then I’m ready to go."
For one peculiar decade, the human computer served as the calibration layer for the electronic one. Then the handover was complete, and the qualifier changed sides.
Once, the machine needed the adjective: electronic computer, automatic computer. Today, the human being needs it: human computer, mental arithmetic. Watch where the adjective sits, and you can date the moment a civilization surrenders a word.
Mathematics is living through its Katherine Johnson decade. When a language model coupled to a formal proof assistant generates an alien, hundred-thousand-line proof of a conjecture, senior mathematicians are summoned to the console. They are asked to check that the hypotheses were not subtly relaxed, that the formal definitions in Lean match what the mathematical community actually meant, and that the proof accepted by the kernel is an argument that can be translated into human thought. For this fleeting interval, the human mathematician is the calibration layer for the solver.
Katherine Johnson’s role ended; orbital mechanics flourished. If mathematicians spend this decade clinging to the adjective’s old seat, the phrase that emerges next will be human proof, uttered in the same quaint, artisanal tone with which we now say hand-woven cloth or mental arithmetic. But the interval is precious. It is the brief window in which a community can decide which part of its work it is willing to let the machine inherit, and which part it insists on keeping under the unmarked name of thought.
Two-thirds of a solution
Tyler Cowen is using the right economics, and the history of technology contains a case that cuts directly against the Luddite trap.
In 1979, Dan Bricklin created VisiCalc, putting the first electronic spreadsheet on a personal computer. Before VisiCalc, changing a single revenue projection in a five-year financial plan meant days of pencil recalculation by teams of ledger clerks. When recalculation became instantaneous and free, the common sense of the era predicted the extinction of the financial profession.
Instead, the opposite occurred. As Planet Money documented, between 1980 and 2015 roughly four hundred thousand bookkeeping and clerical jobs disappeared in the United States, while more than six hundred thousand accounting and financial analyst jobs were created.
The new jobs were not the old jobs saved by decree. They were a different species of work entirely. When calculating consequences became cheap, the question "what if?" became free with it. The scarce skill moved one floor up: from the clerical execution of arithmetic to the architecture of the model. Which assumptions are defensible? What depends on what? Which scenario is worth testing on a Tuesday afternoon? The spreadsheet absorbed the syntax of numbers; human beings were suddenly paid to interrogate their semantics.
Yet a spreadsheet total remains human-scale. A person with an educated feel for orders of magnitude can smell a faulty cell. When a famous economics paper accidentally steered global austerity policy on the back of an Excel coding error, a graduate student with working number sense caught the glitch. I have examined that episode elsewhere, and its lesson is clear: judgment is the load-bearing part.
A formal proof assistant fails in a far stranger register. When the Lean kernel accepts a file, the syntax is guaranteed: every step follows from the axioms with absolute mechanical purity. You can be holding a completely verified, 100% correct proof in your hands and still have nothing you can teach to a student, nothing you can explain to a colleague, and nothing that illuminates the structure of the world.
The scarce good in mathematics was never correctness alone. The scarce good is a proof that a finite mind can inhabit.
Terence Tao made this distinction with mathematical precision months before the Navier-Stokes controversy erupted. In April 2026, he broke down mathematical problem-solving into three distinct stages: proof generation, proof verification, and proof digestion. Digestion, in Tao’s taxonomy, means understanding the architectural core of an argument, situating it within the existing literature, simplifying its machinery, and discovering what else it reveals.
For two and a half millennia, the profession never had to separate these stages. A mathematician who spent seven years generating a proof and verifying its steps had, by necessity, digested it along the way. Understanding was the inescapable byproduct of the physical labor. It required no separate line on an academic CV, because you could not reach the summit without walking the trail.
Automated tools spend that byproduct. When generation and verification are mechanized, a proposed proof is at best one-third of a solution. A proof verified by a formal kernel reaches two-thirds. But it remains trapped at two-thirds until someone performs the labor of digestion.
Tao’s rule of thumb for the missing third is disarmingly concrete: a human being can stand up in a room, give a talk, and answer the questions that follow.
In May, Tao gave the failure mode its rightful name: proof indigestion. And he rejected the facile technological fix of training an AI model on a readability rubric to smooth over the prose. His metaphor was culinary: putting a meal through a blender makes it effortless to swallow, but it ceases to be food. The blender has its place; but the race to churn out pre-masticated slurry cannot substitute for the art of cooking.
We saw what the alternative looks like in August, when Tao published his digestion of Sendov’s conjecture. Researcher Lech Mazur had produced a breakthrough formal proof in Lean spanning approximately 90,000 lines of code. It was a staggering computational triumph, but in its raw state, it was unreadable. Tao spent days with the file, combining frontier AI tools with pen and paper, stripping away redundant scaffolding and uncovering the hidden core of the argument.
The resulting digested proof came in at 15,000 lines: elementary, luminous, resting on the fundamental theorem of algebra and classical inequalities. And because Tao had digested it rather than merely compiling it, the proof did something the 90,000-line file had failed to do: it established a stronger, unproved conjecture by Phelps and Rodriguez, settling Sendov’s conjecture in full.
The 90,000-line file was a certificate. The 15,000-line digestion was mathematics.
This is where the VisiCalc analogy reaches its true altitude. When theorem verification costs zero, the demand for human digestion explodes. Cowen has identified the economic space: filling in the blanks of understanding. Tao has supplied the operational test: standing up in the seminar room and answering the questions.
If you have ever held a technically valid proof that you could not defend under the gaze of your peers, you have experienced the unpaid third. The institutions worth keeping are those that refuse to mistake a two-thirds certificate for human understanding. As I have argued in The Claim Upon the Training Data and The Fiction Layer, authority is conferred, not computed. A machine can emit a valid output. It cannot stand behind it. In mathematics, standing behind an output has a technical name: it is called digestion.
Mourning the assurance
The loss that mathematicians feel is real, and it deserves to be honored before it can be outgrown.
For centuries, the entry ticket to mathematical discovery was paid in solitary, grueling years of lemmas. It was an extortionate tax. Countless brilliant intuitions were strangled in the cradle because a single human life was too short to check the edge cases. No one in their right mind should mourn the sign error that consumed a graduate student's youth.
Yet that tax bought something beyond correctness. It forged a person who had lived inside a problem long enough that the idea became a second nature, a way of seeing. The heroic portraits we carry of Euler, of Gauss, of Grothendieck, or of the quiet colleague down the hall who never won a medal, are portraits of that solitary formation. When verification becomes a cloud commodity, that apprenticeship loses its monopoly.
To pretend that nothing has died is the shallow cheer of the technologist. But to try to resurrect that world through institutional declarations is what Henry David Thoreau recognized in Walden as the tragedy of lives lived in quiet desperation: mistaking the friction of an old tool for the spirit of the enterprise.
In Our Late Spring, I examined how the philosopher Stanley Cavell understood mourning. For Cavell, mourning is not a clinical depression or a pathology to be cured by finding a quick replacement; it is the demanding, courageous acknowledgment that a world we once inhabited has slipped away from us.
Cavell observed in his study of classic comedies, Pursuits of Happiness, that ancient societies trusted their public ceremonies (such as weddings) to guarantee that human continuity and commitment would persist. But when historical catastrophes shook those foundations, society stopped believing that any outward ceremony could guarantee the future. What remained, Cavell wrote, were our "capacities for improvising a world, beyond ceremony."
The open letters and petitions of 2026 are ceremonies whose guarantees have expired. They are the academic equivalent of trying to forbid modernity from entering the room by passing a resolution. They appeal to corporate benevolence because the community has not yet found the courage to mourn its lost monopoly.
Thoreauvian mourning asks for something far sturdier. It does not ask us to deny the loss, nor does it ask us to retreat into cynical defeat. It asks the mathematician to lower their head, acknowledge that the solitary struggle with the lemma is no longer the sole guarantor of truth, and then, with clear eyes, wake up to the morning.
Mourn the assurance. Let the solved problem cease to be the sole measure of a thinker's stature. Improvise the institutions that know how to honor a 15,000-line argument that teaches over a 90,000-line file that merely compiles. That work is unglamorous and slow: deciding who gets hired, which papers count, and whether a scholar is rewarded for turning an opaque machine proof into an insight that another human being can love.
Tyler Cowen is entirely right that the mathematical community is free to do this today. But freedom is only the threshold. The habit of digestion is what a community either builds or loses while it is busy mourning the wrong thing.
Beyond ceremony
This is why utilitarian defenses of mathematics, however well-intentioned, point in the wrong direction. Po-Shen Loh has suggested that we justify human mathematicians by casting them as the cybernetic guardians of interconnected software, steering complex networks against rogue AI attacks. But if the ultimate justification for pure mathematics is that its practitioners make competent flight controllers for digital infrastructure, we have reduced the most sublime adventure of human thought to an auxiliary branch of systems engineering.
The true justification is older and sturdier.
When the pocket calculator arrived, we did not stop teaching children arithmetic. We continued teaching long division not because children could out-calculate a silicon chip, but because number sense is the irreplaceable substrate of judgment.
When Deep Blue defeated Garry Kasparov in 1997, chess did not wither. Today, more than 250 million people play the game across the globe. Grandmasters routinely interrogate neural engines for novel lines, yet nobody pays admission to watch two cloud servers battle in silence. We gather to watch finite human beings think under the relentless pressure of a ticking clock, navigating their own limits, daring to make a move that they alone must answer for.
Mathematics is standing on the threshold of its own great emancipation:
The democratization of the frontier: For centuries, advanced mathematics was gated by the brutal apprenticeship of formal technique, accessible only to those who could spend a decade at an elite academy. When formal verifiers become conversational partners, inquiring minds across the globe will be able to test their structural intuitions without begging a tenured gatekeeper for permission.
The renaissance of exposition: For generations, elite research universities have starved teaching and exposition, treating pedagogical clarity as a distraction from the production of novel lemmas. When lemma generation is automated, the mathematician who can illuminate, synthesize, and convey mathematical taste to others will finally be recognized as the beating heart of the discipline.
The expansion of the horizon: Relieved of the crushing weight of manual verification, the human mathematician is finally freed to become what she was always meant to be: not a mechanical calculator of steps, but an architect of concepts, a composer of structures, an explorer of forms.
Tyler Cowen was right that the market will not preserve an artisanal monopoly out of nostalgia. But the market, left to its own devices, knows only the price of an output; it has no concept of what an understanding is worth.
Mathematics was never merely an engine for generating cryptosystems or modeling fluid dynamics. It is the language through which finite, mortal creatures discover the intelligible contours of reality and share that wonder with one another.
The machine has taken the proof. The understanding remains ours to forge.