AI FOR SCIENCE · INTERVIEWS
Three mathematicians whose fields these results land in each read their own: Kontorovich says the quasi-Riemann statement was already in Mathlib, so he is fully confident the proof is right, and its moves are all known tools of analytic number theory; Moitra says the Unique Games proofs are 'not very readable', with no new idea easy to point to; Brunton says the Navier-Stokes result holds in a regime that is not physical, and engineering fluid computation has not changed.
The timeline records the release and the first reactions, Kontorovich's 'instant Fields Medal' among them; this episode gives the judgments of people in each field after reading the results one by one: which formal statement can be trusted, which proof people cannot yet read, and which result has no bearing on applications.
These are reactions from days after the release; all three say they are still digesting it, and Kontorovich says he still has technical details to go through himself. Nobody checked all 722 manuscripts, and most of the episode is their judgment.
Kontorovich says he did not expect to see the quasi-Riemann hypothesis proved in his lifetime. He is '100% confident' the proof is right, because its Lean statement was already in Mathlib, not written by OpenAI, and the proof leaves nothing unfinished. He has read the proof at a high level: embedding the Möbius function and twisting it by sextic characters are the 'bread and butter' of analytic number theorists, chained in just the right order. The result is a whole vertical strip with no zeros between real part seven-eighths and one, and a second proof reaches about eleven-twelfths. He says the method fundamentally cannot get down to one half, which would be the full Riemann hypothesis, and that needs a new idea. In the same episode he says earlier that it is 'not a genuinely new idea' and later that quasi-RH 'needed lots and lots of new ideas, and it came up with that'.
“The Lean statement was already in the library, was already in Mathlib, so the fact that they have a sorry-free proof gives me 100% confidence that the proof is right.”Alex KontorovichMoitra says that when he entered the field the Unique Games Conjecture was still argued both ways, with opinion shifting year to year through the 2010s; Dor Minzer and Irit Dinur proved the weaker 2-to-1 version, and he had thought humans might need another 10 to 20 years. OpenAI's release says it is true. He says rumours had circulated for weeks, and Minzer wrote in a paper's footnote that the rumours pushed him to post his approach early. He says the proofs are 'not very readable' and it is hard to point quickly to the key new idea; the work now is digesting them. He adds that hours before the release he asked Subhash Khot, who posed the conjecture, whether he would read a positive proof, and Khot said no.
“they're not very readable papers. It's not like you can point to them and really quickly identify what's a new key idea.”Ankur MoitraBrunton is an engineer who works on fluids. He describes the AI's construction: a specialised vortex filament stretched in the third dimension and thinned, its radius shrinking at a particular rate, so the fluid's total energy stays finite while vorticity becomes infinite along the filament, like a figure skater who spins faster by pulling in their arms. He says he was already surprised when mathematicians, before the AI proof, began to think such a counterexample could be found. But by the time the blow-up happens the scale is so small that it is no longer a fluid and the equations themselves stop holding. So 'day-to-day engineering fluids' is almost completely unchanged: designing a wing or an artificial heart still takes supercomputers and wind tunnels. In his words, a million-dollar maths problem was solved and a trillion-dollar engineering problem remains: predicting flows fast and doing inverse design.
“it operates at a regime that's so non-physical that it doesn't really affect my day-to-day engineering.”Steven BruntonKontorovich says he gave a colloquium in Princeton's mathematics department explaining that AI could build only one or two layers on top of Mathlib, 'jerry-rigging', and two days later Anthropic posted a 13-million-line Lean proof of Fermat's Last Theorem from the axioms; 'everything I said in that colloquium was wrong'. Fermat's statement is elementary enough to check at a glance, so there is no question of whether the formal statement matches. He says the proof is not clean and needs much more work to reach Mathlib quality; but whether a proof people have written on paper can be turned into a formal proof with nothing left unfinished is, he thinks, a problem that is done.
Moitra says OpenAI reportedly prompted thousands of problems and released only the positive solutions, about a ten percent success rate, so nobody can see which problems fall and which do not. He worries about two more things: the safest problems seem to be those that plainly need a new idea, and once someone shares that idea an AI can exhaust what follows from it, so mathematicians may become more secretive; and someone has to review all these AI papers, for which he wants collaborative ways of verifying rather than the already overloaded journals.
The timeline's entry on OpenAI's 722 manuscripts says a Lean proof checks each step, not that the formal statement is the open problem, and quotes Kontorovich's 'instant Fields Medal'.
Kontorovich says the quasi-Riemann result happens to escape that problem: its statement was in Mathlib before OpenAI. He also says the method cannot reach one half, and that a second proof reaches about eleven-twelfths.
The timeline records OpenAI's Navier-Stokes claim (a finite-time singularity under smooth forcing), the priority dispute and the Clay Institute's statement, with nothing from someone in fluids on what it means physically.
Brunton says the blow-up happens at scales where the equations no longer describe a fluid, so the result matters mathematically and does not touch engineering fluid computation.
The 722 entry has Altman saying the Unique Games result has a Lean proof, and nothing from a complexity theorist who has read it.
Moitra says the result is true but the proofs are hard to read, with no key new idea easy to point to, and that Khot, who posed the conjecture, said he would not read them.
The 722 entry says the model was given about 4,000 open problems.
Moitra points out that only the successful tenth was released and the failures were not, so the line between what the AI can and cannot solve cannot be seen.
Within the same release, the quasi-Riemann statement was already in the community's Mathlib and Fermat's can be checked at a glance, which is why Kontorovich trusts them fully; other statements were written by OpenAI itself, or there is no formalisation at all. When reading an AI maths result 'verified in Lean', the first question is whether the statement existed before the result.
Moitra's example is Anthropic's 3SUM result: a basic problem thought hard turns out to have a faster algorithm, and knowing that alone forces fine-grained complexity theory to reorganise. On the other side, if the Unique Games proofs cannot be read, the field gets no new tool to use on neighbouring problems. So a result's value to a field has two parts: the conclusion, and whether the proof carries an idea that can be taken elsewhere.
Brunton's view is that the Navier-Stokes result tells us more about the equations, but fluid engineering is stuck on something else: there is no small set of numbers, like temperature, pressure and density for a gas, that describes turbulence, and he calls finding one a good problem for AI. When reading that AI solved a hard problem about a physical equation, it helps to ask whether it solved the mathematical question or the one engineers actually have to compute.
The quasi-Riemann proof is right, because its Lean statement was already in Mathlib and the proof leaves nothing unfinished.
Guest's judgment
Kontorovich's judgment; he says he still has technical details to go through, and this page did not check the statement in Mathlib.
The quasi-Riemann proof uses only known moves, chained in a new way.
Guest's judgment
In the same episode he also says it 'needed lots and lots of new ideas'; both are in the transcript.
The quasi-Riemann method cannot get down to one half, so it cannot prove the Riemann hypothesis itself.
Guest's judgment
Kontorovich's judgment.
The Unique Games proofs are hard to read, with no key new idea easy to point to.
Guest's judgment
Moitra's view shortly after the release.
Rumours that Unique Games had been solved circulated weeks before, and Minzer mentioned them in a paper's footnote.
Industry context
Moitra's account; this page did not find the footnote in two of Minzer's recent arXiv papers.
OpenAI prompted thousands of problems and released only the successes, about a ten percent rate.
Industry context
Moitra says 'apparently'; consistent with the timeline's figures of about 4,000 problems and 372 result families.
The Navier-Stokes blow-up happens at scales where the equations no longer describe a fluid, and does not affect engineering fluid computation.
Guest's judgment
Brunton's judgment; at one point earlier he says 'existence uniqueness', and later describes a finite-time blow-up counterexample.
Turning a proof people wrote on paper into a formal proof with nothing unfinished is a solved problem.
Guest's judgment
Kontorovich's judgment, resting on Anthropic's Fermat formalisation; he says it is far from Mathlib quality.
An Anthropic result on 3SUM found an asymptotically faster algorithm than any known and changed fine-grained complexity theory.
Industry context
Moitra's account, which he says Virginia Vassilevska Williams and Josh Alman wrote up; this page did not read it and the timeline does not have it.
Whether the Unique Games proof gets an exposition by someone else, or a refereed version, that names the key new idea.
Would show up as A paper or lecture notes by a complexity theorist outside OpenAI.Whether OpenAI publishes the problems it did not solve, so the line between what the AI can and cannot solve can be seen.
Would show up as A list of all the roughly 4,000 problems, with the outcome of each.Whether the quasi-Riemann method is pushed below seven-eighths, or someone shows why it cannot be.
Would show up as A paper improving the bound or proving the method's limit, with a formalisation.Whether any work in fluid computation or inverse design makes use of the Navier-Stokes construction.
Would show up as A paper that cites and uses it on a real flow problem, with a comparison.Later evidence that tests or limits what was said, and targets whose date has passed.
Moitra wants collaborative ways of verifying AI proofs rather than the journals. On 26 October, before releasing a 3-SAT result, OpenAI asked three complexity theorists to organise its examination: Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT, who wrote to their field the same day that their involvement is not certification. It is a first organised review, set up by the company, with no verdict yet.Timeline entry →
In Moitra's own field, OpenAI and Anthropic each claim a subexponential 3-SAT algorithm refuting the Exponential Time Hypothesis, each checked in Lean and neither checked outside. OpenAI's Lean formalises a weaker bound than its manuscript: the gap Kontorovich says the quasi-Riemann result avoided, where the statement Lean checks is not the one the paper claims.Timeline entry →
Read 2026.10.28 What was read is the full transcript on the show's site (which says it is human generated and may have errors), with speakers and timestamps, read in full; the audio was not heard. The date and length come from the YouTube video's metadata; the guests' own references (the results came out 'on Tuesday', 'a few days ago') put the recording within days of the 6 October release. This page covers the parts where the three discuss OpenAI's 6 October results and Anthropic's Fermat formalisation; education, Perelman and the advice to young people are left out. That Moitra is visiting the Institute for Advanced Study this year is the host's introduction; his post is from his own homepage. Moitra says a paper by Dor Minzer carries a footnote about the rumours; this page checked two of Minzer's arXiv papers from September and October and did not find it, so it is recorded as Moitra's account. The Anthropic 3SUM result he mentions was not read. Open the interview ↗Episode page ↗The show's full transcript ↗