There is a rumour moving through the mathematical and AI communities that the Hodge Conjecture has fallen.
The claim concerns the conjecture itself, rather than another special case or clever partial result: one of the remaining Millennium Prize Problems, carrying a $1 million prize and seven decades of failed attempts. The rumour is third-hand, unverified and may be completely wrong. The Clay Mathematics Institute still lists Hodge as unsolved.
That qualification is essential, but it does not make the rumour trivial. A few years ago, “an AI has solved Hodge” would have sounded like science fiction or marketing copy. Now it is plausible enough to circulate among people who know what the conjecture is.
OpenAI said on 8 September that it had heard, on 1 September, rumours that two Millennium Prize Problems had been resolved, which prompted it to direct frontier systems at the outstanding problems. The identity of the second alleged result has not been publicly established. In the online mathematical gossip that followed, Hodge was repeatedly named. One discussion described the claim exactly as it should be described: “third-hand rumor.”
If the rumour is false, another one will come. The important change has already happened. We have reached the point where the sentence “AI may have solved Hodge” no longer disqualifies itself.
That changes the argument about AI and mathematics. The interesting question is no longer whether machines will eventually solve problems once reserved for exceptional humans. It is what happens to mathematics when proof itself stops being the scarce thing.
The hostility tells on itself
Watch the reaction whenever a frontier system produces another serious mathematical result. Alongside the fascination is a surprisingly intense pleasure at the idea that mathematicians might be made obsolete.
The reaction is sociologically more interesting than technologically interesting. Most of the people cheering have never lost a job, a grant or a journal slot to a research mathematician. They are not watching an oppressive monopoly collapse. They are watching a tiny profession of people who spend their lives proving difficult things for salaries that many of them could exceed elsewhere.
Yet the mood often resembles status revenge.
Mathematics is unusually irritating to a culture that has learned how often status can be manufactured. In plenty of fields, connections can masquerade as competence, presentation can hide weak thinking, and confidence can survive for years without ever facing a decisive test. Mathematics is less forgiving. At some point there is a proof, and other people can inspect it.
That made mathematical ability unusually hard to democratise by rhetoric. AI seems to offer a satisfying correction. Intelligence can be industrialised. The intimidating technical skill can be bought by the token. The priesthood loses its magic.
But that reading confuses a skill with the people who possess it. Academic mathematicians did not generally choose academia because industry had no use for them. Quantitative finance and AI are full of mathematicians and theoretical physicists who crossed over. For many of the strongest researchers, staying in mathematics meant declining a much higher market price for their abilities.
AI is not revealing that mathematicians were useless. It is beginning to make one of their rarest outputs cheaper.
And when a technology makes one layer of a value chain cheap, value moves towards the next bottleneck.
For mathematics, that bottleneck is increasingly judgment.
Proof is becoming cheaper
For most of modern mathematical history, an important proof bundled several achievements together. The mathematician had found a worthwhile problem, understood the relevant structure, selected or invented the right tools, persisted through technical dead ends and produced an argument that other experts could interrogate. Usually, possession of the proof was strong evidence that the intellectual route to it belonged largely to the person whose name sat above the paper.
AI is separating those things.
Independent benchmarking already shows systems solving research-level problems rather than only olympiad exercises. First Proof was designed around previously unpublished problems specifically to reduce the chance that a model could retrieve a known solution from training data. Its organisers have continued running new batches because a single static benchmark ages quickly at the frontier.
Individual successes matter less than the industrial cost curve now forming around proof production. More compute buys more parallel attempts. Agent systems can pursue many approaches at once, compare partial results, search literatures, test constructions and feed candidate arguments into automated checking. They do not get bored. They do not need to protect a favourite idea. They can spend enormous effort on an avenue that a human would abandon because the opportunity cost is too high.
Terence Tao has described the shift as a move from “proof scarcity” to “proof abundance”. His 2026 essay asks what the human goals of mathematics become when formal mathematical output is no longer difficult to produce in the old way.
That framing is more useful than asking whether AI will “replace mathematicians”. Professions rarely disappear because one output becomes cheaper. They reorganise around the work that remains difficult.
The trouble is that mathematics has spent centuries using hard-won proof as a proxy for several other things it values. Once that proxy breaks, the profession has to say more clearly what those other things are.
An oracle that cannot explain its own education
The comparison with Go gets us only so far.
When AlphaGo produced moves that elite players would never have considered, humans could study them and eventually absorb some of their logic. But the move was ultimately vindicated by the game: it helped win.
A mathematical proof has a different afterlife. It enters a network of human knowledge. Other mathematicians read it, compress it, teach it, generalise it, connect it to other structures and eventually make the once-difficult argument feel inevitable.
AI could therefore be extraordinarily valuable to mathematicians even if machines become better theorem provers than people. A sufficiently explicit machine-generated proof can be inspected line by line. A mathematician can reconstruct the technique and emerge better equipped than before.
The educational relationship is strange. Human mathematicians may end up learning from a teacher that can produce the lesson without being able to give a reliable human account of how it came to know what mattered.
This distinction becomes obvious with very large formal proofs. Anthropic, for example, reported that Claude largely autonomously produced the first complete computer-checked formalisation of Fermat’s Last Theorem. The project took 11 days and produced roughly 13 million lines of Lean, including tens of thousands of intermediate theorems. That is an extraordinary compression of labour. It is not, by itself, a compression of understanding.
A giant correct proof can still be poor mathematics in the intellectual sense. It can bury the useful idea under thousands of mechanically necessary steps. It can give the same rhetorical weight to a profound reduction and a routine estimate. It can prove a theorem without helping the reader see why the theorem was true.
Tao makes a related point about human proofs. Their awkwardness contains information. The lemma that took pages to tame, the notation that changed halfway through, the section an author had to rebuild: these traces tell another mathematician where the difficulty lived. A polished machine proof can sand away exactly that signal.
So the scarce product moves. If proofs become cheap, explanation becomes more valuable. If machines become excellent explainers, problem selection matters more. If machines become good at choosing problems, then theory building and mathematical taste become the next frontier.
Humans may not own that frontier permanently. Systems are already being built to assist with conjecture selection, research direction and theory formation. The durable claim is narrower: humans still need mathematical taste now, and we may be removing the process that produces it faster than we learn how to replace that process.
The apprenticeship paradox
Mathematical taste is not something a student acquires by reading a list of principles. It is built through repeated contact with difficulty.
You choose the wrong abstraction and discover why it was wrong. You spend months on a lemma that collapses after somebody notices a simpler route. You learn that a page of ugly calculation may be routine while an innocent-looking reduction contains the whole problem. Over time, the pattern of your mistakes becomes part of your judgment.
Some of the apparent drudgery is itself part of the education.
This creates an apprenticeship paradox. The better AI becomes at removing the painful intermediate work required to become a mathematician, the harder it may become to produce humans capable of supervising mathematics at the highest level.
A surgeon is not trained merely to produce successful routine procedures as efficiently as possible. Residency builds judgment through exposure to cases, mistakes, uncertainty and repetition. If a machine can perform the routine procedure better, the training problem does not vanish. It becomes harder to design.
Tao has raised essentially the same concern about mathematics. There are educational settings in which using AI to eliminate the struggle defeats the point, because the answer was never the only product of the exercise.
This is the flaw in the comforting “convex hull” metaphor. Imagine existing human mathematics as a vast space. Machines become superb at exploring its interior, combining known techniques, joining remote literatures, testing constructions and filling gaps. Humans remain responsible for pushing the boundary outward by inventing new structures and new questions.
It is a nice division of labour, until you ask where the next generation of boundary-pushers comes from after twenty years of removing the training that produced the previous one.
The metaphor also assumes that AI remains inside the hull. We do not know that it will. First Proof’s organisers explicitly distinguish proving well-formed statements from harder tasks such as selecting questions, formulating definitions and developing new theories, and they argue that those higher-order abilities also need evaluation.
The reassuring version of the future therefore depends on two assumptions: machines will not learn mathematical taste, and humans will keep learning it even after machines remove much of the work through which people acquired it. Neither is secure.
The moving boundary of “real mathematics”
The dismissals that follow each new result have become repetitive.
The model used existing techniques. The problem was unusually machine-friendly. The theorem matters less than understanding. The system did not invent a new field. It needed too much compute. Humans still had to verify the argument, choose the problem, interpret the result.
Some of these objections are good objections. Taken together, however, they reveal a definition of “real mathematics” that keeps retreating towards whatever machines have not yet done.
Technological substitution rarely arrives as a single cinematic event. It moves task by task. Systems solve contest problems, then unpublished lemmas, then open problems. They assist research programmes, generate conjectures, rank candidate directions, search for analogies and improve their explanations. No ceremony marks the day the profession has changed. The old boundary simply stops matching the work.
The Hodge rumour belongs in this story even if it dies tomorrow.
There is still no public basis for saying the conjecture has been solved. Clay lists the crucial dimension-four case as open. But imagine a credible 200-page manuscript appearing tomorrow under an AI lab’s name. The first serious questions would probably concern verification, provenance, compute, authorship and formalisation. The possibility that a machine generated it would no longer be the unbelievable part.
That is a profound change in expectations, and expectations change institutions before capability has finished changing reality.
The last cohort of the old regime
The title of this essay is deliberately unfair. Future mathematicians will earn their achievements too, and some may have to earn them in ways that are harder to measure.
What is ending is a particular bargain between mathematical labour and mathematical credit: the great theorem obtained through an overwhelmingly human chain of cognition, with the scars of the proof belonging to roughly the same mind whose name appears on it.
There are mathematicians alive now whose careers were formed entirely under that bargain. They may be the last.
The next generation will work with AI-assisted conjectures, machine-written lemmas, automated literature searches, formal verifiers and agent swarms exploring hundreds of approaches while the human collaborator sleeps. Some arguments will have intellectual lineages that are difficult to reconstruct because the system generating them was trained on an enormous fraction of the mathematical literature.
Attribution is already becoming an institutional problem rather than a matter of etiquette. The Leiden Declaration on Artificial Intelligence and Mathematics calls for disclosure of automated tools, human responsibility for correctness and serious attention to the provenance of machine-assisted ideas. The International Mathematical Union has endorsed it. A separate registry, Palomar, has been created for Lean-verified mathematics as the volume of machine-assisted formal work rises.
Those institutions are early responses to a world in which producing a proof and establishing what the proof means, where it came from and who deserves credit for it are no longer the same job.
Prestige will have to move accordingly. The mathematician who closes a problem may matter less than the one who chooses the right problem, invents the useful language, recognises the one valuable result among ten thousand generated candidates or compresses a monstrous formal artefact into an idea other humans can use.
Universities will also have to resist a tempting form of efficiency. Students may need to prove things that machines can prove faster, calculate things machines can calculate perfectly and spend a week on arguments an agent can produce before lunch. That will look wasteful if education is measured only by output.
But apprenticeship is not supposed to maximise output. It is supposed to produce the person who can later judge output.
The Hodge rumour may turn out to be nonsense. A proof may appear tomorrow, in five years, or much later. The rumour has still revealed something. One of the most intimidating sentences in mathematics, “Someone has solved the Hodge Conjecture,” now invites an immediate follow-up: human or machine?
At the start of this decade, that question would have sounded absurd. Soon it may sound quaint.
Mathematics will not run out of propositions. There will always be another theorem, another structure, another problem beyond the current frontier. The danger lies elsewhere. If proof becomes abundant enough, we may stop paying the cost of producing people who know what proofs are for.
The machines would keep producing mathematics. The volume could become enormous. The formal correctness could improve. Yet the human community able to rank, explain, connect and care about those results could grow thinner.
The greatest intellectual project in human history could end up drowning in answers while running short of people able to tell which questions deserved them.
Sources
Clay Mathematics Institute, Hodge Conjecture page; OpenAI, 8 September 2026 account of the Millennium Prize rumours and subsequent research push; First Proof research-level benchmark and project materials; Terence Tao’s 2026 essay on proof abundance and the future goals of mathematics; Anthropic’s report on the Lean formalisation of Fermat’s Last Theorem; Leiden Declaration on Artificial Intelligence and Mathematics; International Mathematical Union endorsement of the Leiden Declaration; Palomar registry for Lean-verified mathematics.