Grant Sanderson – AI and the future of math

Grant Sanderson (creator of 3Blue1Brown) joined Dwarkesh to map how recent AI advances are reshaping mathematical research and what that implies for the broader economy. Sanderson frames mathematics as one of the clearest 'spikes' in current AI capability: problems are verifiable, often grindable in deterministic environments, and lend themselves to massive parallelization. He uses the International Mathematical Olympiad (IMO) as a concrete benchmark: modern systems handled geometry problems extremely fast (Grant reported geometry solutions on the order of ~19 seconds in a 2024 run) but still struggle with combinatorics — the latter being the wildcard that cost an AI a potential gold in 2024. That combination illustrates his central heuristic: progress is uneven across subdomains, and passing a big benchmark will likely be another step rather than an epochal discontinuity.

The conversation then explores how AIs might tackle the deepest open problems, using the Riemann Hypothesis as a running example. Sanderson distinguishes three qualitatively different solution modes: (1) cross-domain bridging — analogous to the Hugh Montgomery and Freeman Dyson anecdote where number theory and random-matrix statistics converged; (2) 'mountain-building' — the kind of heavy theoretical edifice that underpinned Wiles’s proof of Fermat's Last Theorem via elliptic curves and modular forms; and (3) brute-force, extremely long proof that yields little conceptual compression. He emphasizes the implications: bridging-style solutions suggest the same abilities that help in white-collar tasks (finding novel connections across fields), while mountain-building might be a more specialized kind of mathematical creativity whose economic spillovers are harder to predict.

A major topic was benchmarks beyond theorem-proving. Both speakers worry less about a single binary headline and more about the AI's ability to generate useful conjectures and definitions — the historically highest-value moves in mathematics (e.g., Galois inventing group-based perspectives on solvability). Sanderson stresses the long verification loop for such conceptual innovations: Lagrange to Abel to Galois to 20th-century applications is a century-scale story showing that human verifiers and cultural acceptance take time. He also discusses tooling trade-offs: formal proof assistants like Lean and the Mathlib corpus give an automated, verifiable reward signal and enable 'let it run' experiments that could be left to explore for years; yet many recent advances (including DeepMind's work) also succeeded with natural-language approaches and meta-verifiers that check proofs less formally.

Finally, they address practical consequences for mathematicians and students. Sanderson argues the human role will likely shift toward curation, education, and translating AI outputs into human-understandable explanations — functions where social trust and pedagogy matter. He counsels students to understand where value and funding flow (teaching, institutional prestige, applied math areas like PDEs and simulation) and to consider stable relational roles (teaching/curation/mentorship) even as theorem-proving becomes more automated. Both agreed on technical design ideas for accelerating discovery: ensemble agents with diverse heuristics (some explicitly trying to disprove a conjecture, others to prove) to increase 'entropy' and serendipity, and robust verifier/meta-verifier systems to avoid swamping mathematicians with unreliable proofs. Overall, the episode portrays AI-driven mathematics as both a testing ground for broader AI capabilities and a domain where the interplay of verifiability, parallelizability, and human curation will determine whether machine discoveries become comprehensible, useful, and economically transformative.