I’m not a mathematician, but engineering and economics qualifications put me on the same branch of the academic disciplines tree. Mathematicians have had a bad time recently, and I feel for them. On 6 October 2026 OpenAI dropped 722 mathematics manuscripts onto GitHub. An unreleased internal model was set roughly four thousand open maths problems, with about three hours of compute for each result. The papers that survived were grouped into 372 families.
The results are a big deal: the Unique Games Conjecture is a problem in computational complexity that has resisted proof since 2002. Only some papers arrived with Lean formalisations - translations of the proof into computer code, so that software can check every step mechanically. OpenAI itself warned that some of the unformalised proofs could contain errors.
Within a day three manuscripts were withdrawn and fourteen others revised. Almost everything withdrawn or substantially revised sat outside the Lean-checked part of the repository. Alex Kontorovich of Rutgers said that a human who produced the same body of work would win an instant Fields Medal. Other mathematicians asked the question: how do you referee hundreds of papers from a model nobody else can run? In science, replication is part of the process. Nobody outside OpenAI can replicate this.
The big stink came fast: within a day, some mathematicians were calling for a boycott of OpenAI. The obvious next step, though, is for humans to check the machine’s work. Proof assistants change what checking means. When an AI hands you a fifty-thousand-line Lean proof, the software verifies every inference. What returns is logically sound, but nearly unreadable. Intermediate ideas that a human needs in order to follow the argument are often missing or buried.
Compare this with the humanities. In 1623 John Heminges and Henry Condell collected thirty-six plays by their dead friend Shakespeare and published them as the First Folio. Eighteen of those plays had never been printed. Several others survived only in pirated “bad quartos” stitched together from actors’ memories. Some of the Folio texts were set from foul papers: the author’s messy working drafts, short on punctuation. Without Heminges and Condell, Macbeth and The Tempest would be lost. Without three centuries of scholars untangling the syntax and explaining the hard passages, much of what survived would still be unreadable.
For a long time elite mathematicians thought of themselves the way we once thought of Elizabethan playwrights: solitary geniuses producing proofs out of thin air. That self-image is ending. The working mathematician of the near future will look increasingly like a senior literature professor sitting with the First Folio.
William Thurston saw this change coming more than thirty years ago. In his 1994 essay “On Proof and Progress in Mathematics” he insisted that the real product of the subject is human understanding. Formal proof is only a means. Once truth becomes cheap and automatic, the bottleneck shifts to interpretation.
Mathematicians will become textual editors. Faced with a long machine proof they do the same work a Renaissance scholar does with a damaged manuscript: cut redundant detours, regularise the notation, compress eight hundred lines of raw tactics into one named lemma and write the equivalent of footnotes. “Here, between lines 400 and 450, the model is exploiting a hidden symmetry that never gets stated.” Status will attach to the ability to rewrite the raw script as a three-page argument a person can hold in the head. Some of this labour already happens with human proofs; AI multiplies the volume and the unreadability.
They will also become critics and curators. Once the cost of producing a correct proof approaches zero, machines will generate millions of true, non-trivial and boring theorems every week. The old status game, proving something hard, collapses when anyone can prompt a system to do it. What replaces it will start to look like literary criticism: rival schools arguing about which machine-generated structures are deep and which are dead ends. The Fields Medal of 2038 might go to the person who explains what a machine’s proof of the Riemann Hypothesis means for physics and for human intuition. The machine that found the proof will not be eligible.
I started my career at McKinsey, so, through learned habit, I group things in threes. Here, three things complicate the “maths as a humanity” picture.
The first is ambiguity. In the humanities ambiguity is the point; a critic can write five thousand words on one line of Hamlet because the line sustains several incompatible readings. In a mathematical proof ambiguity is a fatal flaw. People will still argue about the best way to understand a machine argument, such as whether a step is best seen geometrically or algebraically. But the proof itself either works or it does not. A literary critic can bend a poem to fit a fashionable theory; a mathematician cannot.
A second complication is taste. Mathematicians love parsimony and elegance; they often talk about beautifully simple solutions. Ursula Martin of Oxford said OpenAI was “tossing the community a messy first draft and expecting us to clean it up.” Some drafts may not clean up. For example, the 1976 computer proof of the four-colour theorem checked nearly two thousand configurations, and fifty years on nobody has found a version a human can check by hand.
Finally we have the issue of who sets the questions. OpenAI’s model worked through four thousand problems that humans had already judged worth asking. Knowing which questions matter remains at the core of mathematical judgement. The machines do not have it. Yet.
English professors would recognise the plot. A tragic hero is brought down by a flaw of character. The mathematicians’ flaw was to stake their pride on the one skill a machine could learn: proving hard things. Worse, they built much of the machine. The linear algebra, optimisation and statistics behind machine learning all came from applied mathematics. Soon their job will be to sit in the library with the AI papers, decoding the strange notation, explaining why the proofs work and getting nostalgic about the days when they wrote them. This is their tragedy.