While some parts of the math community are talking about how the field would suffer if AI generates large numbers of math proofs no one understands, others seem to believe that such proofs will become an integral part of further mathematical research.
Jacob Tsimerman, who won this year’s Fields Medal and then announced he was leaving the University of Toronto to work on AI safety at OpenAI, has laid out a strikingly matter-of-fact vision for where his field is headed: proofs so dense and so machine-dependent that no single person, including the mathematician whose name is on them, can fully account for every step.
Speaking with Curt Jaimungal on the Theories of Everything podcast, Tsimerman compared the situation to something much more mundane than a mathematical proof — a train.
“I think pretty soon we’re gonna have proofs no one understands, and they’re going to underlie mathematics, and based on that mathematics, other things are going to work,” he said. “Does a train run even if no one understands the mechanics by which it runs? Yes, it does. I mean, you can look at it run.”
What makes the comparison land is that Tsimerman isn’t describing some hypothetical future state. He says it’s already true of his own, human-written work.
“I don’t understand all the steps”
Pressed by Jaimungal on whether he meant he simply couldn’t reproduce a proof from memory on demand, Tsimerman said the gap runs deeper than that. He pointed to o-minimality, a tool from logic and model theory that has become central to his own celebrated results, including the proof of the André-Oort conjecture that helped win him the medal.
“I kind of know loosely how they prove that o-minimal structures are all minimal, but I definitely don’t know the proofs, and I definitely couldn’t recreate them,” he said. “Maybe I could if I spent years on it.”
That leads him to a question most working mathematicians would rather not sit with: does relying on results he can’t personally reconstruct mean he doesn’t really understand his own work? His answer is a qualified no. “In some sense, I understand the pieces of it that I contributed. There’s bits that I really thought hard about, which I understand very, very well. But do I understand it from first principles? No.”
It’s a description of how mathematics has quietly worked for a long time — nobody re-derives the whole edifice from Peano’s axioms before publishing a paper — except Tsimerman is extending the same logic to a much less comfortable place: a layer of results that no human, not even a specialist, could verify by inspection, because they were produced and checked by machines operating on a scale and in a style unlike anything mathematicians have had to accept on faith before.
A field already arguing about exactly this
Tsimerman’s comment lands in the middle of a live and fairly heated argument inside mathematics about whether this is actually a healthy way for the field to proceed. Fields Medalist Terence Tao, who has spent the past two years documenting his own experiments with AI-assisted proofs in detail, has been far more guarded, warning that a famous open problem getting “solved” by an opaque, proprietary AI system could leave the field no further ahead than before, with mathematics worse off for having the box checked.
Tao has gone further still, telling an audience at the same International Congress of Mathematicians where Tsimerman received his medal that if authors can’t give a clear talk explaining their own results, those results probably shouldn’t be published at all — pointing to sites like erdosproblems.com, which he said already hold dozens of AI-generated submissions that are likely correct but remain unverified by anyone willing to vouch for them.
Tsimerman’s own position is more sanguine, and it’s one he’s been building toward since before he joined OpenAI. He has said AI will soon do everything mathematicians do, only better and faster, treating that less as a threat to the profession than as a shift in what the profession spends its time on.
The record so far
The backdrop to this debate is a run of results that have made the “no one fully understands it, but it works” framing harder to wave away. OpenAI’s models generated proofs to 300+ math problems last week, that led to much opposition — and soul searching — in some mathematical circles.
Whether any individual researcher, Tsimerman included, could walk through every line of those proofs unaided is, by his own account, beside the point. The train runs. What’s being negotiated now, in public, between people like Tsimerman and Tao, is what happens to a field built for centuries on the idea that someone, eventually, has to be able to explain why.