All podcasts / Dwarkesh Podcast / Summary

Grant Sanderson (@3blue1brown) - AI disproved a famous math conjecture. Now what?

2026-06-30 - 76 min - source - Read full transcript

Dwarkesh Patel (host)Grant Sanderson

Key insights

AI math progress is driven as much by 'grindability' as by verifiability.

Dwarkesh argues verifiability alone doesn't explain why AI races ahead in math and code but crawls in computer use, even though checking a package delivery is also verifiable. The missing ingredient is grindability: math and code can be cheaply parallelized into thousands of deterministic rollouts (spin up a container, try a fix, compare diffs), while real-world domains like browsing a bot-detected website or running a business can't be replayed and farmed the same way.

verification-and-grindability

Formal verification in Lean turned out to matter less to recent AI math progress than expected.

Both point to DeepMind's IMO system moving from Lean-based proofs in its first year to natural-language proofs the next, and to the unit distance conjecture disproof having no Lean in its released chain of thought, as evidence that process-based formal verification is not the main driver. Natural-language verifiers checked by a meta-verifier (as in DeepSeek's published methodology) appear to work almost as well.

verification-and-grindability

There are three qualitatively different ways AI could solve a big open problem, with very different human-legibility.

Grant distinguishes 'lightning bolt' connections between two fields an expert can immediately parse (like the unit distance result), 'mountain building' that requires an entirely new theoretical apparatus (like Fermat's Last Theorem's reliance on elliptic curves and modular forms), and raw brute-force chains of reasoning with no new theory. Only the last risks producing correct-but-undigestible proofs; mountain-building risks the fate of Mochizuki's disputed 'inter-universal geometry' attempt on the abc conjecture, where years of human effort might still turn out to be climbing the wrong mountain.

ai-math-progress

If AI automates theorem-proving, the scarce human skill shifts from proving to defining and conjecturing.

Grant cites the framing that 'good mathematicians prove theorems, great mathematicians come up with conjectures, and the greatest mathematicians come up with definitions,' and argues this reframes what a benchmark for AI math progress should even look like: not a pass/fail goalpost but a subjective tone shift in how working mathematicians describe a model's usefulness in deciding what to study in the first place.

future-of-mathematicians

Mathlib gives math a training-loop advantage nothing else has: fully unsupervised, indefinitely-running exploration.

Because Lean-verified proofs need no human check-in (unlike natural-language math, which still needs a human to confirm a result is meaningful), Grant proposes an AI could be set loose on a fork of the Mathlib repository, run for years without supervision, and generate its own conjectures and definitions the way AlphaGo/AlphaZero explored Go on its own. The open question is whether anything useful emerges, and how you'd even evaluate the output.

verification-and-grindability

Historical precedent for how long a genuinely novel abstraction takes to be validated: Galois theory took roughly a century.

Lagrange first suggested symmetry of polynomial roots might be the right lens (with no result attached), Abel independently proved quintics unsolvable, and Galois's own notes were rejected multiple times and only recognized as valuable twenty years after his death, then formalized into modern group theory another twenty years after that. Only in the 20th century did Gell-Mann's group-theoretic prediction of quarks demonstrate practical payoff. This 'verification loop' is far too slow and subjective for any current RL training signal.

ai-math-progress

AI's structural edge over even a great human mathematician may be parallelization and deliberate entropy injection, not raw intelligence.

Dwarkesh notes digital minds can universally apply their capability across every accessible problem at once rather than relying on one idiosyncratic genius, and can be spun up with deliberately different biases (prove it vs. disprove it, different starting heuristics) to escape the shared context and assumptions that can trap a field, similar to how the unit distance conjecture reportedly stayed unsolved partly because researchers assumed it was true and mostly tried to prove it.

ai-math-progress

Grant expects mathematicians to end up functioning like museum curators rather than becoming obsolete.

Even in a world where AI proves theorems and explains them clearly, Grant argues humans will still want a trusted human curator navigating a near-infinite space of ideas worth engaging with, because the motivation to care about a topic is a social phenomenon (comparable to why people still value human musicians despite objectively 'better' synthesized audio being possible).

future-of-mathematicians

Career advice for a field facing AI disruption: understand where the money and prestige actually come from, not just whether you're good at the work.

Grant argues too few students entering math (or any field) trace the actual economic/social chain: brand value to a university, NSF grants as a public-good proxy, or direct teaching value. He predicts teaching specifically is one of the more AI-resistant careers over the next fifty years because it is fundamentally relational and coaching-oriented, not just explanatory.

future-of-mathematicians

AI writing lags math and code because writing's output IS the substance, and requires modeling a specific reader's mind.

Unlike code (any implementation that passes tests is fine) or a lemma (any valid proof works), each word and sentence of writing directly constitutes the value, so it can't be 'sloppy but functional.' Good writing also requires anticipating exactly what a specific reader is thinking at each moment, a form of theory-of-mind that autoregressive next-token generation seems poorly suited to, since it resists the deliberate unpredictability that makes writing insightful.

ai-writing-and-learning

LLMs currently behave like Wikipedia for learning: broad and mostly correct, but missing single-author, motivated narrative structure.

Grant contrasts LLM explanations with single-author references like the Princeton Companion to Mathematics or the Stanford Encyclopedia of Philosophy, which deliberately sacrifice some local correctness for narrative motivation. His main current use of LLMs is as a souped-up search engine to find the right human-written resource (he was once gaslit by an LLM inventing a fake 3Blue1Brown video citation). Dwarkesh's most productive study method pairs a human-authored textbook or lecture (which sequences ideas correctly) with an LLM used only to prune confusion around that spine.

ai-writing-and-learning

LLMs can't yet do what a top-tier human teacher does: reframe a student's flawed question instead of just answering it.

Both agree that when a learner asks a question revealing a wrong mental model, the best human teachers 'jujitsu' the student's own framing toward the right one, while LLMs tend to be sycophantic ('what an insightful question') and simply run with the question as posed. Grant links this to the same theory-of-mind gap behind AI's writing weaknesses, and speculates it could close in roughly five years.

ai-writing-and-learning

Books referenced

Nonlinear Dynamics and Chaos - Steven Strogatz - Dwarkesh describes studying this textbook alongside Strogatz's lectures and an LLM, calling it bliss and comparing it to Grant's videos in book form
The Princeton Companion to Mathematics - edited by Timothy Gowers - cited as an example of a single-author-crafted reference (versus crowdsourced Wikipedia) that deliberately motivates ideas rather than just stating correct facts

Media referenced

Unit distance conjecture explainer - video - Grant references a video by math YouTube channel Polylog explaining the unit distance problem that an AI later found a counterexample to
The Fall of the Theorem Economy - article - David Bessis blog post Dwarkesh cites arguing theorem-proving has historically gotten outsized credit relative to definition- and problem-creation, which AI progress may invert
Unsolved expository problem (essay on forcing) - article - Grant cites mathematician Timothy Chow's essay proposing that some proven results (like the continuum hypothesis via forcing) remain unsolved as expository/explanatory problems even once proven
Stanford Encyclopedia of Philosophy - other - cited alongside the Princeton Companion as single-author-curated references that beat Wikipedia's crowdsourced, correctness-first style for building understanding
Spaced-repetition prompt-writing report - paper - Andy Matuschak and a collaborator's report on trying (and largely failing) to get LLMs to write good spaced-repetition flashcards, used as evidence LLMs struggle to model a specific reader's future mind
Karpathy's auto-research LLM speed-run project - other - Dwarkesh references Andrej Karpathy's experiment where LLM agents modified a single training script and kept changes only if they sped up the run, as an early model of unsupervised research loops
Eric Jang episode on AlphaGo - podcast - Dwarkesh recalls a prior episode where Eric Jang explained AlphaGo, and notes such systems are good at pursuing one line of research but bad at abandoning dead ends
DeepSeekMath paper - paper - Dwarkesh cites DeepSeek's published methodology for training a natural-language math verifier checked by a meta-verifier, as evidence process supervision can work without Lean
Grant Sanderson's first Dwarkesh interview (2023) - podcast - the pair revisit Dwarkesh's original IMO-gold question to Grant from their first conversation three years earlier
Dwarkesh's interview with Dario Amodei - podcast - Dwarkesh recalls asking Dario two-to-three years earlier why AI couldn't yet connect known facts into a new discovery, a question this episode revisits given the unit distance result

Companies

OpenAI - credited with the headline-making disproof of the unit distance conjecture counterexample discussed throughout the episode
DeepMind - cited for its IMO gold-medal system, which used Lean the first year and switched to natural language the next, evidence Lean was less essential than assumed
DeepSeek - its DeepSeekMath model and published training methodology are cited as evidence that natural-language proof verification with a meta-verifier can work without formal languages
Boeing - referenced via a mathematician's PDE-simulation insight that reportedly saved Boeing billions by reducing physical build-test-rebuild cycles

Techniques and frameworks

RLVR (reinforcement learning with verifiable rewards) - the training paradigm discussed as central to AI math/code progress, and as the reason human-legible 'why is this idea good' questions are hard to train for
Grindability - Dwarkesh's proposed second driver of AI math/code progress beyond verifiability: math and code (unlike computer use or business strategy) can be cheaply parallelized into thousands of deterministic rollouts
Lean / Mathlib formal proof system - discussed as a way to get automated, unsupervised verification of math claims; Grant proposes an AI could run indefinitely extending Mathlib without human check-ins
Galois theory / group theory - used as the episode's extended case study of how a genuinely novel abstraction (symmetry of polynomial roots) took roughly a century, through Lagrange, Abel, and Galois, to be recognized as valuable
Langlands program - Grant frames as a research ethos of preemptively finding connections across seemingly unrelated fields of math, distinct from just solving named problems
Kolmogorov complexity / compression as elegance - floated as a possible way to reward AI for compressed, human-understandable proofs rather than just brute-force-correct ones

Summary

Dwarkesh Patel and Grant Sanderson (3Blue1Brown) revisit a question from their first interview three years earlier: once AI gets gold at the International Math Olympiad, is that AGI? Grant's original answer, that it would turn out to be just another benchmark, held up, and the episode opens by dissecting why math keeps producing the fastest, most legible AI progress of any field, this year highlighted by an AI-found counterexample to the decades-old unit distance conjecture. Dwarkesh proposes that verifiability alone doesn't explain the gap with domains like computer use; what math and code share is grindability, the ability to cheaply run thousands of parallel, deterministic rollouts, which real-world tasks like browsing a bot-protected website or running a business can't replicate. Both push back on the assumption that Lean and formal verification are the key driver: DeepMind's IMO system dropped Lean between its first and second year, and the unit distance disproof's chain of thought contained no Lean at all, suggesting natural-language verification with meta-verifiers (as in DeepSeek's published work) is doing more of the work than expected.

A large stretch of the conversation is a case study in how hard it is to reward or benchmark genuinely novel conceptual progress, using the century-long path from Lagrange's symmetry-of-roots hunch through Abel's impossibility proof to Galois's rejected, then rediscovered, notes that eventually became modern group theory. Only in the 20th century, with Gell-Mann's group-theoretic prediction of quarks, did the idea's practical value become obvious. That kind of "verification loop" is too slow and subjective for current RL training, which is exactly why Grant expects the next hard benchmark for AI in math to be conjecture- and definition-generation rather than theorem-proving, quoting the framing that "great mathematicians come up with conjectures, and the greatest mathematicians come up with definitions." Grant also floats a distinctly math-only possibility: because Lean-verified proofs need no human check-in, an AI could be set loose to extend the crowdsourced Mathlib repository indefinitely and unsupervised, similar to how AlphaZero explored Go on its own, with no guarantee anything useful comes out the other end.

The two also discuss what makes AI's advantage over individual human genius structural rather than just a matter of raw intelligence: it can apply the same capability level in parallel across every accessible problem, and can be deliberately given different starting biases (prove it vs. disprove it) to escape the kind of shared assumption that reportedly kept mathematicians trying to prove the unit distance conjecture true for years before someone tried disproving it. On the flip side, both spend real time on why AI writing lags math and code so badly: code and math have flexible "end products" where any correct implementation works, while writing's output is directly the substance, and good writing requires modeling a specific reader's mind moment to moment, a form of theory-of-mind that autoregressive generation seems structurally bad at (illustrated by an aside about Botox recipients becoming worse at reading others' facial expressions once their own face stops mirroring emotion).

The episode closes on the human role in a world of increasingly capable AI mathematicians. Grant argues mathematicians will likely become something like museum curators, valuable not because AI can't prove or explain things but because the motivation to care about a topic remains a social, trust-based phenomenon, the same reason human musicians retain value despite technically "better" synthesized audio being possible. His broader career advice, aimed at students worried AI will make their field pointless, is to trace where the actual money and prestige in a job come from (university brand value, grant-funded public good, or direct teaching) rather than assuming being good at the work guarantees a role; he specifically predicts teaching will be one of the more AI-resistant careers over the next fifty years because of its relational, coaching character. On learning with LLMs specifically, Grant compares current LLM explanations to Wikipedia: broad and largely correct but missing the deliberately motivated narrative arc of a single expert author, and describes his most common use of LLMs as a smarter search engine pointing him to the right human-written resource (with a cautionary story about being confidently pointed to a fabricated 3Blue1Brown video). Dwarkesh's most effective study method pairs a well-sequenced human text or lecture with an LLM used only to resolve local confusion, since neither agrees LLMs can yet do what the best human teachers do: reframe a learner's flawed question instead of just answering it as posed.

Notable Quotes

"Good mathematicians prove theorems, great mathematicians come up with conjectures, and the greatest mathematicians come up with definitions." - Grant Sanderson

"The dirty secret with the IMO is that you really can train for a lot of them." - Grant Sanderson

"You build a man a fire, and he's warm for one night. But set a man on fire, and he's warm for the rest of his life. So that's where I am with AI." - Grant Sanderson

"It's like an alien trying to empathize. How could it have theory of mind?" - Grant Sanderson

"There's really no fundamental difference between a benchmark and a training environment." - Dwarkesh Patel