#503 – AI Crisis in Math: Navier-Stokes, Riemann Hypothesis & Complexity Theory

What It Covers

Lex Fridman convenes mathematicians Steven Brunton (University of Washington), Ankur Moitra (MIT), and Alex (Rutgers) to analyze OpenAI and Anthropic's release of roughly 700 AI-generated mathematical proofs — including the quasi-Riemann hypothesis, Navier-Stokes existence-uniqueness, and Fermat's Last Theorem formalization in 13 million lines of Lean code — and what this means for the future of mathematics as a human discipline.

Key Questions Answered

• •The Convex Hull vs. Semigroup Distinction: When evaluating AI mathematical breakthroughs, resist dismissing them as "inside the convex hull" — meaning linear combinations of known ideas. Mathematician Alex argues the semigroup framing is more accurate: AI chains known mathematical moves in sequences so long and precise that no human team could have executed them. The quasi-RH proof used cubic theta functions and Mobius function techniques known for decades, but assembled in a cascade that shocked every expert in the field.
• •The Doorman Fallacy Applied to Mathematics: Avoid reducing a mathematician's role to theorem-proving alone — this mirrors the "doorman fallacy," where automating a job's most visible task (holding a door) misses its full value. Mathematicians also build new theories, identify generative questions, forge cross-field connections, mentor researchers, and communicate ideas through narrative. When theorem-proving becomes cheap via AI, these orthogonal contributions become proportionally more valuable, not obsolete.
• •The Solved Axiom as a Planning Tool: Alex proposes a thought experiment called the "solved axiom" — assume any problem solvable by a human-AI team could also be solved by AI alone. Even accepting this hypothetical, pure mathematics retains value because mathematical knowledge living in human minds differs fundamentally from proofs stored in data centers. Use this axiom not as a prediction but as a forcing function to clarify what human mathematical contribution actually means beyond proof generation.
• •Lean Formalization as the New Verification Standard: Anthropic's Fermat's Last Theorem formalization — 13 million lines of Lean code, produced by two to three people with no domain expertise — establishes that auto-formalization of written mathematical results is effectively solved. Any theorem humans have written down can now be converted to a sorry-free Lean proof. Researchers should treat Lean verification as the new baseline for proof validity, replacing community peer review as the primary trust mechanism for AI-generated results.
• •Quasi-RH Establishes a Zero-Free Vertical Strip: Prior to this proof, the known zero-free region of the Riemann zeta function narrowed as the imaginary part increased, unchanged for 70 years. The AI proof establishes a full infinite vertical strip — no zeros exist where the real part falls between seven-eighths and one. The methods used cannot extend to the one-half line required for the full Riemann hypothesis, meaning a genuinely new mathematical idea is still needed to close that gap.
• •Blueprint Collapse for Graduate Training: The standard PhD roadmap — take a problem the community cares about, improve it incrementally, publish in top venues — no longer functions reliably when AI resolves hundreds of open problems simultaneously. Advisors should shift mentorship toward breadth of mathematical thinking, metacognitive delegation (deciding what to assign to AI versus retain for human reasoning), and identifying questions that generate productive research programs rather than optimizing for individual theorem credits.
• •Openness Norms Under Pressure: The mathematics community's tradition of sharing ideas freely faces a structural threat: once a key missing ingredient enters the literature, AI can potentially combine it with existing results to complete a proof autonomously. Researchers may begin withholding novel conceptual ideas longer than before, mirroring competitive dynamics in other fields. Counteracting this requires developing new attribution and contribution models — similar to MathLib's pull-request system — that reward idea generation separately from proof completion.