Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472
Terence Tao explains why Navier-Stokes blowup, twin primes and Collatz remain open, how Lean and AI change proof work, and what it takes to tackle problems on the solvable/hopeless boundary.
Key takeaways
10 points- 1Engineer simplified models that blow up to reveal which features any true regularity proof must exploit.
- 2Finitize infinite claims to restore intuition and obtain explicit quantitative bounds.
- 3Isolate one difficulty at a time; solve nine turned-off versions before reintroducing complications.
- 4Formalize proofs in Lean when collaboration or future edits are likely; change cost drops sharply.
- 5AI currently excels at computation and verification but lacks reliable intuition for viable proof strategies.
- 6Twin primes resist statistical attack because they can be deleted without disturbing aggregate prime statistics.
- 7The parity barrier caps almost-prime density proofs at 50 percent with present sieve technology.
- 8Switch problems or add strategic assumptions rather than emotionally locking onto one intractable conjecture.
- 9Try anything, however stupid, once standard techniques fail; the community often supplies the missing piece.
- 10Mathematical progress is cumulative; centuries of prior work enabled Wiles's proof of Fermat's Last Theorem.
Summary
Terence Tao maps the frontier between solvable and hopeless problems in mathematics and physics while charting how AI and formal tools are reshaping proof work.
Kakeya, Waves and Navier-Stokes
- The Kakeya conjecture links needle-turning puzzles to wave concentration that can focus energy into singularities (0:00-12:01).
- Tao engineered blowup in an averaged Navier-Stokes equation by selectively disabling interactions, proving that any global-regularity proof must exploit features the averaged model lacks (12:03-24:04).
- Supercritical PDEs let nonlinear transport dominate dissipation at small scales, making blowup possible though never observed in real fluids.
Infinity, Models and Universality
- Finitizing statements (e.g., finite monkeys typing Hamlet) restores intuition and enables quantitative estimates (36:06-48:09).
- The Central Limit Theorem produces Gaussian universality, yet systemic correlations destroyed that assumption in the 2008 crisis (48:12-1:00:13).
Formal Proofs and AI
- Lean forces pedantic verification but isolates changes so a single constant edit updates only affected lines (1:24:21-1:36:24).
- A 22-million-pair algebraic-implication project used 50 mathematicians plus Lean; only two pairs remain open (1:36:25-1:48:28).
- AlphaProof reached IMO silver but still collapses under combinatorial explosion in long proofs (1:42:51-1:57:37).
Prime Conjectures and Barriers
- Twin primes are sparse enough that deleting 0.01 percent leaves all statistical tests intact, blocking aggregate methods (2:17:30-2:34:04).
- The parity barrier caps almost-prime density at 50 percent, ruling out current sieve techniques for twin primes and Goldbach (2:24:45-2:36:48).
Productivity and Advice
- Structured procrastination and switching problems prevent emotional lock-in on single intractable questions (2:55:16-3:06:17).
- Try anything, however stupid, once standard moves fail; the community on MathOverflow functions as collective super-intelligence (3:06:17-3:14:23).
Deep read
Executive Summary
Terence Tao’s Lex Fridman interview navigates the frontiers of mathematics, physics, and the evolving role of AI and formal proof systems in mathematical discovery. Tao dissects what constitutes a “hard” problem, foregrounding the Kakeya problem, Navier–Stokes regularity, and the critical/supercritical regime that complicates global regularity proofs. He illustrates how averaging strategies illuminate why certain approaches fail, and how a deeper, structural lens—through concepts like energy transfer, wave packets, and turbulence—frames where breakthroughs might occur. The discussion expands to the interplay between mathematics and physics (symmetry, conservation laws, Hamiltonian mechanics) and to the ambitious potential of AI-assisted theorem proving via Lean and the Mathlib library, including the Equational Theories Project and the prospect of large-scale, distributed mathematical collaboration. Tao emphasizes that the human creative spark remains central for conjecture formation and theory-building, while AI and formalization tools promise to revolutionize verification, collaboration, and experimentation. Across these threads, the interview sketches a pragmatic path forward: embrace structured exploration, deepen understanding of universality and structure, and leverage tooling to extend mathematical reach without sacrificing the rigor and elegance that define the discipline.
00:00:00 Introduction
Speaker: Lex Fridman
- Lex Fridman introduces the guest, Terence Tao, highlighting his stature as one of history's greatest mathematicians, Fields Medal winner, Breakthrough Prize winner, and contributor across numerous mathematical and physical disciplines.
- This section frames Tao’s breadth: Navier–Stokes, analytic number theory, harmonic analysis, compressed sensing, random matrix theory, combinatorics, and progress on hard problems.
"Terence Tao is widely considered to be one of the greatest mathematicians in history..."
00:50:00 Major Topic: The First Hard Problem
00:50:00 Subtopic: What counts as a truly hard problem?
- Tao reframes the notion of hardness: the boundary between what can be done with existing techniques (roughly 90% of a solution) and the missing 10% that requires a new stroke of insight.
- He cites the Kakeya problem as a formative example early in his research where boundary cases challenge standard methods.
- The Kakeya problem origin traces to a 1918 puzzle by Soichi Kakeya: rotate a needle in the plane with minimal area; Besicovitch showed you can do this with arbitrarily small area in 2D, later extending to 3D with a thickness delta.
- In 2D, everything is understood; in 3D, finite-thickness constraints (delta) complicate the problem, and the minimal-volume function of delta is conjectured to be slow (logarithmic) in delta.
- Connections: Kakeya links to PDEs, number theory, geometry, and combinatorics, including wave propagation, where wave packets resemble tubes and their focusing vs defocusing behaviors mirror energy concentration questions.
- He connects to Navier–Stokes as a Millennium Prize Problem: questions about existence and smoothness of solutions to incompressible Navier–Stokes are tied to the kind of “concentration vs dispersion” phenomena discussed in Kakeya-like constructions.
> "What are problems where existing techniques can do like 90% of the job, and then you just need that remaining 10%?"
01:25:00 Subtopic: An explanatory bridge to Navier–Stokes
- Tao discusses averaging the Navier–Stokes equations to isolate specific nonlinear interactions and see whether singularities (blowups) can occur under controlled rules.
- He purposely designs an averaged model where certain energy-transfer channels are disabled, forcing energy to move scale-by-scale in a controlled way to potentially blow up in finite time.
- This engineered model serves as an obstruction to approaches that could solve the real Navier–Stokes problem; if a technique works on the averaged version but not on the true system, that exposes gaps in those approaches.
- Core ideas: dissipation (viscosity) vs transport (nonlinear advection); the problem sits in the supercritical regime where small scales see stronger transport than dissipation.
- Fundamental terms:
- Global regularity: velocity field remains smooth for all time. - Finite-time blowup: a singularity where velocity becomes unbounded in finite time. - Supercritical vs critical vs subcritical: how nonlinear effects scale relative to dissipation across scales; supercritical means nonlinear effects dominate at small scales, making analysis harder. - Energy cascade: distribution of energy from large scales to small scales, tied to turbulence dynamics.
- The 2D Navier–Stokes problem is (classically) “critical” rather than supercritical, with techniques turning regularity more tractable.
> "The key phenomenon that my technique exploits is what's called supercriticality."
02:35:00 Major Theme: Why persistence of regularity is hard
- Tao emphasizes that many attempted global regularity proofs fail due to hidden or subtle signs of blowup; the averaging trick exposes which approaches cannot possibly work on the true system.
- He uses the Maxwell’s demon analogy: even if energy transfer looks statistically possible to tame, a contrived microscopic configuration could in principle lead to improbable singular behavior. In mathematics, such conspiracies must be ruled out or accommodated.
- The metaphor of pi’s digits is used to illustrate a potential hidden bias (a demon) in seemingly random sequences; proving their absence is nontrivial.
- He explains that while turbulence dampens energy and promotes regularity, a special initial state could concentrate energy so quickly that viscosity cannot temper it.
- The aim of his averaging work is to isolate why standard approaches fail, thereby guiding where real global regularity proofs would need to exploit features of the actual equations.
- Distinguishing concept: supercritical equations push the nonlinearity to small scales more aggressively than dissipation, making the flow hard to control and driven toward potential blowup.
> "Maxwell's demon is a concept in thermodynamics... this is a situation that shows up a lot in mathematics."
03:50:00 Subtopic: Analogy bridges and the “galactic” scale of idea-building
- Tao uses a circuit analogy to describe building a blowup mechanism: from physics to a hypothetical liquid computer where water acts as computational media; gates and a clock trigger energy transfer through a cascade to smaller and smaller scales, forming a blowup chain akin to a Turing machine built with fluid dynamics.
- He mentions his thought experiment of a fluid von Neumann machine: a water-based system capable of building smaller copies of itself, transferring energy to a smaller version, then powering down, creating iterative self-replication that could mimic blowup behavior.
- The practical obstacles are many: physical realization of logic gates with fluids, error correction in analog computing, and maintaining isolation of large-scale from small-scale dynamics.
- The Game of Life (Conway) as a conceptual inspiration: simple local rules yield complex global structures (gliders, guns, self-replicators), illustrating emergent computation in a discrete setting that informs thinking about continuous systems like fluids.
- He emphasizes a duality: mathematics can unify disparate domains when the underlying formal structure aligns, even across continuous vs discrete models.
- The key takeaway: local rules generating surprising global behavior reinforce the possibility that micro-level engineering could inform macro-level phenomena—though actual fluid implementations pose enormous technical challenges.
> "The Game of Life is a simple system... it shows it's possible to build almost anything with the right gates."
04:50:00 Subtopic: Structural vs Randomness dichotomy in math
- Tao discusses a central theme in modern math: structure vs randomness. In many areas, either an object has a clear structure or behaves essentially randomly; inverse theorems identify when a pattern is due to hidden structure.
- Szemerédi’s Theorem (1970s) states that any set of integers with positive density contains arbitrarily long arithmetic progressions. The theorem holds even in random-like (pseudorandom) sets, showing a robust form of structure that persists under randomness.
- He uses the infinite monkey theorem to illustrate how, in infinite sequences, every finite pattern will eventually appear almost surely, but finite realizations require enormous data and careful analysis.
- The art, he argues, is finitarizing infinite results to obtain quantitative, finite bounds and intuition that helps in concrete problems.
- He distinguishes between pure structure theorems and probabilistic arguments that reveal how randomness emerges in large systems.
- Example: central limit theorem, which explains why many random processes converge to Gaussian distributions, highlighting universality in large-scale behavior.
- This framework motivates how Tao views universality and emergent phenomena in physics and mathematics alike.
> "Szemerédi’s Theorem concerns trying to find a certain type of pattern in a set of numbers... any sufficiently large set of positive density contains arithmetic progressions of any length."
06:15:00 Subtopic: Infinity in math and engineering intuition
- Tao discusses the role of infinity in mathematical reasoning and how finitizing infinite statements often yields more intuitive proofs and practical insights.
- He notes the trade-off: finite, constructive versions can be messier, but they offer concrete rates and finite bounds that aid intuition and verification.
> "Infinity absorbs a lot of sins."
07:15:00 Major Topic: Mathematics vs Physics vs Engineering
- The conversation pivots to the philosophy of science: the tripartite relationship between the real world, observations, and mathematical models.
- Tao emphasizes mathematics stays within a model and explores the consequences of that model, whereas physics emphasizes predictions to match observations; both are crucial and complementary.
- He contrasts the theoretical dominance in mathematics with the experimental emphasis in physics, noting recent growth in experimental mathematics and the potential for AI to scale experimental exploration.
- The balance of top-down (theory-driven) and bottom-up (data-driven) approaches is highlighted as essential for breakthroughs.
- He cites the compressive viewpoint: a successful theory compresses vast observations into simple, parameter-light models; the beauty of mathematics often lies in this compression principle.
- The discussion circles back to Noether’s theorem (symmetry implies conservation laws) and the Hamiltonian formulation as unifying structures across classical and quantum mechanics.
> "Mathematics stays within the model, and we ask what predictions would the model make... compression of the universe into a simple theory."
08:55:00 Subtopic: The role of symmetry and language in physics and math
- Noether’s theorem is invoked as a paradigm for how symmetry yields conservation laws, and how similar Hamiltonian structures underpin both classical and quantum theories.
- Tao opines that a shared mathematical language (Hamiltonian formalism) helps bridge classical and quantum intuition, guiding the transfer of insights like energy conservation and symmetry to quantum contexts.
- The struggle to reconcile general relativity with quantum mechanics is discussed in terms of needing new mathematical concepts beyond standard Cartesian coordinates; the Hamiltonian viewpoint gives a direction for where future theories might emerge.
- The prevailing confidence: a theory of everything is plausible, but the path is nontrivial; the current theories (GR and QM) are extremely successful, so breakthroughs require new mathematics and new physical insight.
> "The Hamiltonian behind classical mechanics also is the key object in quantum mechanics... when you have the right language, it clarifies both domains."
10:10:00 Subtopic: Perelman, Ricci flow, and solving deep geometry problems
- Tao shifts to the geometry/topology frontier via Grigori Perelman’s work on the Poincaré conjecture, which uses Ricci flow with surgery to classify 3-manifolds.
- He outlines the historical progression: Ricci flow smooths geometric structures, similar to heat diffusion; in 2D, flow leads to spheres (classic results). In 3D, the problem is supercritical and can develop singularities; Perelman introduced reduced volume and entropy functionals to convert the problem to a critical regime where singularities can be analyzed and treated surgically.
- Tao recounts a personal anecdote about a transformation of the wave maps equation (a nonlinear PDE) using a gauge-like transformation to stabilize dynamics, a technique akin to a coordinate change that reveals linear behavior in a nonlinear system.
- The overall theme: deep problems often require new invariants or structural insights that recast the problem into a tractable (often critical) regime.
- He emphasizes how Perelman’s work required years of sustained effort and deep understanding of singularities, directions that AI currently cannot replicate at scale.
> "Perelman introduced reduced volume and entropy... turning a supercritical problem into a critical one where nonlinearities look less scary."
11:45:00 Major Topic: Learning and problem-solving strategies
- Tao discusses his approach to difficult problems: use strategic, minimal perturbations (the “cheating”) to strip away multiple difficulties, solve a simpler version, then reintroduce complexities gradually.
- He likens problem-solving to choreographing a fight scene: many potential opponents, but you fight them one by one, not all at once.
- The pen-and-paper habit remains central for him, though he increasingly uses blackboards and, gradually, computational aids for exploration and verification.
- He underscores the value of visual thinking and bespoke diagrams (hand-drawn doodles) on blackboards; the process is organic and iterative.
- He notes the rising role of automated tools like Lean and Mathlib for formal verification, with real-time collaboration at an atomic granularity, enabling distributed teamwork on proofs.
> "The beauty of mathematics is that you get to change the problem, change the rules as you wish... a mathematician can do whatever they want."
01:24:00 Subtopic: Lean, formal proofs, and AI-assisted proof systems
01:24:21 Lean as a proof assistant
- Lean is a formal proof programming language that can produce certificates for proofs, offering a verifiable trace of reasoning.
- Distinction: Lean is executable like a traditional programming language, but it also proves theorems by generating a proof certificate, with Mathlib as a large library of formalized mathematics.
- The process is more pedantic: every object has a type, and Lean enforces precise definitions and justification steps; this makes formalization robust but sometimes tedious.
- The formalization workflow allows very large collaborations with a formal self-checking backbone, enabling distributed verification across dozens of contributors.
> "Lean is a computer language... it can produce not just the answer, but a proof that how it got the answer as three plus four equals seven."
01:38:00 Subtopic: The role of AI in Lean and mathematical practice
- Current AI use in Lean is largely leveraged as autocomplete, code-suggestion, and search within Mathlib; few examples exist where AI fully generates a formal proof from scratch.
- The bottleneck: proof reading and verification remain human-intensive; the formality overhead (type-checking, complete justification) is substantial.
- A demonstrated benefit: automating the verification of parameter adjustments in a formalized proof (e.g., replacing a constant from 12 to 11) reduces re-verification effort massively; only a handful of lines need updating.
- The collaboration angle: Lean enables highly granular collaboration; large groups can contribute pieces of a proof with trustless verification, creating a scalable, distributed proof workflow.
- He notes that formalization will likely lead to a phase shift where papers are written directly in Lean, or Lean-assisted authoring becomes standard in reproduction and refereeing.
> "What you can do with Lean is that in your headline theorem you change a 12 to 11... the compiler shows which lines break and which hold."
01:58:00 Subtopic: The Equational Theories Project
- Tao describes a massive collaborative project: generate 22 million pairwise tests among ~4,000 algebraic laws to determine implication relationships, with proofs or counterexamples for each pair.
- About 50 contributors participated; the effort demonstrates how crowdsourced formal reasoning can tackle combinatorially large mathematical investigations.
- Almost all pairs have been settled; only two remain, with one of those two still being resolved via pen-and-paper proofs and then formalized.
- The project illustrates how aggressive formal reasoning workflows, underpinned by Lean and AI tooling, can transform large-scale mathematical exploration.
- This project also highlights governance of authorship: moving away from traditional alphabetical or single-author conventions to author-inclusive models with detailed contribution matrices.
> "The project was to determine the entire graph of which laws imply others... 22 million problems, 50 authors."
02:40:00 Subtopic: Will AI ever win Fields Medal-level math?
- Tao reframes the question: AI assistance may accompany Fields-level work in the future, but the credit and creative breakthroughs remain human-driven for now.
- He forecasts a near-term future (by 2026) where AI assists with proofs and computations in math papers; this would not necessarily replace human insight but accelerate verification, computation, and literature review.
- He emphasizes the need for robust evaluation of AI-generated mathematics, noting current risks like hallucination of citations and misattribution.
- He envisions future shifts: a potential adoption of Lean-first writing or AI-aided proof development, reducing friction in formalization and refereeing, enabling longer, more complex papers to be produced and checked efficiently.
> "By 2026, there will be math collaborations with AI... not necessarily ideas, but computations and verifications."
03:55:00 Subtopic: The future of mathematical collaboration and education
- Tao notes the potential for mass collaboration via formal proofs, with thousands of contributors coordinated through Lean and Mathlib, akin to modern software dev pipelines (widgets, modular proofs, verifiable components).
- He stresses the social and philosophical dimension: collaboration scales with reliable tooling; the culture must value distributed, verifiable contributions as part of academic credit—this will require a rethinking of authorship norms.
- He believes that the next phase of mathematical discovery will blend human intuition with AI-aided computation, literature review, and automated proof-search, but with the human in the loop for creative breakthroughs and conjecture generation.
> "We can crowdsource proofs at an atomic scale, enabling thousands of contributors with trustable results."
04:50:00 Closing on AI and mathematics
- The conversation loops back to practical questions: what is the unique human contribution in mathematics, and where will AI be most useful? Conjecture generation, discovery of new connections across fields, and high-level strategic planning may be AI-aided in the future, but the generation of novel, deep theories remains a fundamentally human pursuit for now.
- Tao contemplates a future where AI helps with proving old theorems, generating new conjectures, and assisting with new representations, but the human spark—intuition, taste, and a sense for mathematical elegance—remains essential.
06:50:00 Resources Mentioned (summary of materials and tools discussed)
- The discussion references several environments and resources used to advance mathematical research, including:
- Lean theorem prover and the Mathlib library for formalized mathematics. - The Equational Theories Project (massive, crowdsourced algebraic-identity testing via Lean). - The practice of formalizing famous theorems (e.g., Fermat’s Last Theorem) in Lean (Kev in Buzzard and others collaborating). - The Game of Life as a metaphor for emergent computation and structural design from local rules. - The concept of universal patterns and structure-vs-randomness in number theory and combinatorics (Szemerédi, Green–Tao).
- Sponsor mentions and public resources appear throughout the intro and sponsor segments:
- Notion, Shopify, NetSuite, LMNT, AG1 (sponsors of the Lex Fridman podcast).
- Books, blogs, and media:
- Terence Tao’s Blog: https://terrytao.wordpress.com/ - Terence Tao’s YouTube: https://www.youtube.com/@TerenceTao27 - Terence Tao’s Books: https://amzn.to/43H9Aiq
08:10:00 Notable Visuals and Diagrams (described)
- No explicit slides or figures are shown in the transcript; the images described are primarily conceptual diagrams:
- Besicovitch-type constructions visualizing how a needle can be turned with arbitrarily small area in the plane, and a modified, thin-tube version in 3D. - Energy transport tubes and wave-packets visualized as light rays focusing and defocusing; energy concentrating into a space-time region could signal blow-up. - The Game of Life’s gliders and guns serve as a mental picture for emergent computation from simple local rules. - A hand-wavy schematic of a fluid Turing machine: gates built from fluid pulses, a clock, and energy transfer that yields iterated self-replication.
09:30:00 Notable final quotes and remarks
- The host closes with a Galileo quote on mathematics as the language of the universe and Tao offers reflections on the beauty and universality of mathematical structure across domains.
10:15:00 Resources Mentioned (recap)
- Terence Tao’s public materials and links above; ongoing Lean/Mathlib work; Game of Life; Szemerédi’s Theorem and Green–Tao theorem; the Riemann Hypothesis and P = NP as central challenges; Grigori Perelman and the Poincaré Conjecture; Wiles and Fermat’s Last Theorem; Euler’s identity as a beauty exemplar in mathematics.
10:40:00 Summary of the episode's core themes
- The hardest problems in mathematics arise at the boundary of current capabilities; understanding supercriticality and criticality in PDEs clarifies why many problems resist standard techniques.
- Formal proof systems (Lean, Mathlib) alongside evolving AI assistance promise a future in which collaborative, large-scale, rigorously verified mathematics becomes more scalable.
- The interplay between physics and mathematics—through invariants, conservation laws, and unified formalisms (Hamiltonian, Noether)—provides a blueprint for unifying theories and guiding new discoveries.
- The prime numbers (and related conjectures) reveal both the power and limits of current techniques; probabilistic models (random models) offer intuition, but deep conjectures (Twin Prime, Riemann) require breakthroughs that we cannot yet predict with certainty.
Resources Mentioned
- Terence Tao’s Blog: https://terrytao.wordpress.com/
- Terence Tao’s YouTube: https://www.youtube.com/@TerenceTao27
- Terence Tao’s Books: https://amzn.to/43H9Aiq
- Lean Prover: https://leanprover.github.io/
- Mathlib documentation: https://mathlib.readthedocs.io/
- Game of Life (Conway): classic cellular automata example
- Szemerédi’s Theorem: foundational result in combinatorics on arithmetic progressions
- Green–Tao Theorem: primes contain arbitrarily long arithmetic progressions
- Navier–Stokes equations: incompressible fluid dynamics and regularity problems
- Poincaré Conjecture and Ricci Flow: geometric topology and Perelman’s work
- Fermat’s Last Theorem and Wiles
- Euler’s identity and Noether’s theorem (conceptual references)
- The Equational Theories Project: large-scale algebraic-identity testing via formal proofs
- Notable sponsors: Notion, Shopify, NetSuite, LMNT, AG1
Major Topics (tags)
- Mathematics
- AI & Proof Systems
- Physics & PDEs
- Geometry & Topology
- Number Theory
- Computation & Collaboration
Action Items
- Finitize infinite statements to regain intuition and enable quantitative estimates.
- When stuck, turn off nine difficulties and solve the remaining one first.
- Switch problems or add strategic assumptions rather than locking emotionally on one conjecture.
- Try anything, however stupid, once standard moves fail.
- Use Lean early for collaborative or long-lived proofs; the cost of later changes drops dramatically.
- Treat AI output as a fast but noisy first draft that still requires human verification.
- Publish partial progress on related problems instead of waiting for the single perfect result.
Mental Models
Glossary
- Kakeya problem
- A geometric problem about turning a needle (unit line segment) in the plane with minimal area, leading to Besicovitch-type constructions that allow turning in vanishingly small areas.
- Besicovitch construction
- A method showing that a needle can be rotated using arbitrarily small area in the plane; extended to higher dimensions with thickness considerations.
- Navier–Stokes equations
- Partial differential equations describing the motion of incompressible, viscous fluids; central to fluid dynamics and the Clay Millennium Prize problem about global regularity.
- finite-time blowup
- A scenario in PDEs where a solution becomes unbounded (blows up) in a finite amount of time.
- supercritical/critical/subcritical
- Categories describing how nonlinear terms scale with respect to dissipation across scales; supercritical indicates nonlinearities dominate at small scales, often leading to instability or blowup; critical/subcritical are easier to manage analytically.
- wave packet
- A localized wave that travels in space and time; in PDEs, useful for visualizing transport vs dispersion phenomena.
- Ricci flow
- A geometric evolution equation (a nonlinear PDE) that deforms the metric of a manifold to smooth irregularities; key to Perelman’s work on the Poincaré conjecture.
- Perelman’s entropy/reduced volume
- Monotone quantities introduced by Grigori Perelman that render certain geometric flows critical, enabling classification and surgical resolution of singularities.
- Noether’s theorem
- A fundamental link between symmetries and conservation laws: each continuous symmetry of a system’s action yields a conserved quantity.
- Hamiltonian mechanics
- A reformulation of classical mechanics where the Hamiltonian (total energy) governs dynamics; central to bridging classical and quantum descriptions.
- Lean (theorem prover)
- A formal proof language and assistant that produces machine-checked proofs; used with Mathlib for formalizing mathematics.
- Mathlib
- A large library of formally verified mathematics used with Lean to build and check proofs.
- Szemerédi’s Theorem
- Any subset of integers with positive density contains arbitrarily long arithmetic progressions.
- Green–Tao theorem
- The primes contain arbitrarily long arithmetic progressions.
- Riemann Hypothesis
- A central conjecture about the zeros of the Riemann zeta function implying strong statements about the distribution of primes; proving or disproving it has vast consequences for number theory and cryptography.
- P vs NP
- A fundamental question in computer science: does every problem whose solution can be verified quickly (NP) also have a solution that can be found quickly (P)?
Notable Quotes
“> What was the first really difficult research level math problem that you encountered? One that gives you pause, maybe?”
“> As a PhD student, the Kakeya problem certainly caught my eye and it just got solved, actually.”
“> Maxwell's demon is a concept in thermodynamics, like if you have a box of two gases... a microscopic demon... could in principle produce an extremely improbable configuration.”
“> Infinity absorbs a lot of sins.”
“> The beauty of mathematics is that you get to change the problem, change the rules as you wish.”
“> The energy inches forward, scale by scale, in such a way that it stays localized at one scale at a time.”
“> I identify mostly as a fox.”
“> The Hamiltonian behind classical mechanics also is the key object in quantum mechanics.”
“> The paradox of the Turing machine in water is a real thing, but the physical realization is far from easy.”
“> By 2026, there will be math collaborations with AI... not necessarily ideas, but computations and verifications.”
“> The Equational Theories Project: 22 million problems... about 50 authors.”
“> The phase shift in formalization will eventually lower the friction to below one: Lean-first writing and AI-assisted proof development becoming standard.”
“> The Poincaré conjecture was solved by Perelman using Ricci flow with surgery; the work required years of deep, solitary, and brilliant insight.”
“> The unreasonable effectiveness of mathematics.”
Topics
More from Lex Fridman Podcast
See all




