AI, Mathematics, and the Future of Discovery

Alex, Ankur Moitra, and Steven Brunton describe their first reactions and changing feelings about AI-reported mathematical results. They discuss excitement, uncertainty, and the particular anxiety for students whose research plans and expectations may be disrupted.

Brunton expresses hope about applying AI to practical problems while acknowledging fears about losing control or meaning. The guests discuss whether knowing a result has been reached can reduce motivation or help people pursue it.

Alex distinguishes the idea of AI solving mathematics from the idea of destroying it. He defines a hypothetical “solved axiom” and argues that pure mathematics may still matter because of the understanding it creates for people.

The guests discuss how mathematicians build general methods and connections, rather than merely reaching a theorem. They consider how humans select questions they find meaningful and whether AI might help reveal structures worth exploring.

The discussion turns to problem selection, exploration, and the risk of reducing mathematics to theorem-proving. Ankur uses the “doorman fallacy” to argue that a job’s visible task does not capture its full value, and describes mathematicians as building theories and new ways of understanding.

The guests consider whether AI changes the value of mathematical beauty, insight, explanation, and communication. They emphasize that asking an interesting, productive question requires mathematical judgment, and discuss the risks of judging work by visible outputs alone.

Ankur discusses how AI results unsettle the familiar route for graduate students to make an impact. The guests consider how hiring, tenure, and research expectations may need to change, and return to generalization and simplicity as mathematical aims.

The guests ask whether AI could automatically discover simple, generalizable laws or choose important questions. They discuss mathematical contributions beyond asking a question or proving a theorem, and whether the hypothetical solved-axiom world is plausible.

Ankur cautions against anthropomorphizing AI and describes adversarial examples as evidence that neural networks can use patterns unlike human reasoning. The guests discuss qualitative differences between AI and human problem-solving and the prospect of collaboration.

The conversation examines whether AI proofs combine known mathematical moves or introduce genuinely new ideas. Ankur explains the convex-hull and semigroup metaphors, and the guests consider how the quasi-Riemann-hypothesis work draws on existing techniques.

The guests note that a short, elementary proof can resolve a problem that had seemed difficult, and that new results change what researchers choose to study. They discuss an Anthropic result on the threesome problem and its implications for fine-grained complexity theory.

Ankur explains why factoring large numbers matters to public-key cryptography and discusses quantum algorithms and post-quantum methods. The conversation considers how results with major practical consequences might be handled and what mathematical work could be kept private.

The guests return to the metaphors for AI’s use of existing knowledge and discuss whether it can make the landscape more visible. They consider how graduate training may need to encourage broader mathematical thinking, while acknowledging uncertainty about hiring and journals.

The discussion considers whether academic contributions may include reusable code, data, and tools as well as papers. The guests compare pressure on journals and referees with the overload of open-source maintainers dealing with many contributions.

Using the checking of Perelman’s work on the Poincaré conjecture as an example, the guests describe how mathematical communities validate and understand a proof. They discuss the limits of the solitary-genius model and the possible need for more collaborative approaches.

The guests discuss possible ways to organize and improve AI-generated proofs, including collaborative review and Mathlib’s pull-request model. They explain how formalization can make mathematical results reusable and how Lean’s type-checking can help prevent incorrect applications.

Ankur explains interactive theorem provers, Lean, and Mathlib, including how formal proof-checking verifies logical steps. The guests distinguish a proof’s correctness from understanding its ideas, and consider what it would mean to receive a proof that mathematicians could not readily interpret.

The guests distinguish constructing a proof from communicating its meaning, using real analysis and the construction of the real numbers as an example. They argue for explanations that tell the story of an idea alongside formal verification, and reflect on the understanding gained by working through a problem.

Alex explains the zeta function and its connection to prime numbers, using signal processing as an analogy for how its zeros encode information. He describes the Riemann hypothesis as predicting that the relevant zeros lie on a central line.

Alex recalls seeing the quasi-Riemann-hypothesis result and explains why it was beyond his expectations. The guests discuss the Lean formalization of Fermat’s Last Theorem, its 13 million lines of code, and the difference between a checked proof and a clean, library-quality one.

Alex describes how his experience with AI-assisted Lean work shaped expectations that were overtaken by the reported results. The guests discuss the reported human involvement and the claim that producing formal proofs of stated theorems may now be a largely addressed task, while noting that mathematical understanding remains important.

Alex describes primes as the basic components of multiplication and explains why knowing a result is true is not the same as understanding why. He outlines the critical strip and explains how the reported quasi-Riemann result gives a zero-free region that falls short of the full Riemann hypothesis.

The guests discuss how AI results have changed their sense of which problems are within reach. They consider whether researchers may protect ideas more closely to avoid giving AI missing ingredients, and weigh that risk against mathematics’ tradition of sharing.

Brunton explains Navier–Stokes as equations for fluid momentum, velocity, and pressure. He discusses why fluids become difficult to predict and how improved turbulence modeling could matter to aircraft, artificial hearts, turbines, and other engineering problems.

The guests discuss why general equations do not by themselves reveal every phenomenon a system can produce. Brunton explains that Navier–Stokes is a model valid at particular scales, and they consider what mathematical blow-up might mean when physical descriptions cease to apply.

The conversation considers whether unusual fluid behavior could be useful for flow control, then turns to the elements in Navier–Stokes: velocity, pressure, momentum, viscosity, and external forces. Brunton describes how these terms represent fluid motion.

Brunton uses simple differential equations to explain how nonlinear growth can produce finite-time blow-up. He describes the role of viscosity and explains that the reported result concerns a way to construct smooth external forcing that produces blow-up.

Brunton explains the three-dimensional vortex construction in the reported proof and contrasts it with two-dimensional flow. He says the result is mathematically important but does not change day-to-day engineering, where predicting and controlling practical fluid flows remains difficult.

Brunton describes turbulence as a multiscale problem in which many scales affect outcomes such as lift and drag. The guests ask whether a compact representation could make turbulent flows more tractable, and discuss combining data-driven search with mathematical insight.

The guests discuss coordinate transformations, vortex interactions, and the difficulty of finding a simple description of complex flows. They consider whether fluid systems can perform complex computations and whether that limits how much they can be reduced.

Ankur introduces the algorithmic perspective on natural systems, while Brunton contrasts weather’s many relevant variables with insects’ ability to fly in turbulent conditions. They discuss robustness, uncertainty, and how biological systems may act effectively without complete models.

Brunton describes strain-sensitive neurons on insect wings and how local responses help insects react to gusts. The conversation briefly speculates about singularities and black holes before the guests take a break and turn to complexity theory.

Moitra introduces satisfiability and explains why checking a proposed solution can be easier than finding one. He describes P versus NP, probabilistically checkable proofs, gap amplification, and how these ideas underpin hardness-of-approximation results.

Moitra explains why the unique games conjecture could organize results about approximation algorithms. He recounts the history of debate and human progress on the problem, then describes the surprise and relief surrounding the reported AI proof.

Moitra worries that rapid solutions may reduce enthusiasm for problems researchers were pursuing and diminish the learning gained on the way. The guests return to play, curiosity, and the need to preserve meaningful ways for young mathematicians to explore.

The guests discuss the struggle involved in long mathematical efforts and the tradition of individual work. Alex describes a collaborative project that developed incrementally over years, where the statement and understanding emerged through the research process.

Moitra describes involving students in areas adjacent to his expertise and working together to understand the central ideas in papers. The guests consider how AI can help people learn new fields while potentially replacing some of the human interactions that support that learning.

The guests discuss the mismatch between students’ short-term anxieties and research projects that may take years. Brunton describes how biology and materials science inform his thinking about fluid dynamics, and the conversation turns to AI’s prospects in biology.

The guests discuss large biological datasets, connectomes, and the complexity of life across scales. They reflect on how humans find useful abstractions in nature and on the surprising effectiveness of mathematics in describing the physical world.

The guests debate whether mathematics is created or discovered, distinguishing the questions people choose to ask from the answers they find. They discuss mathematical abstraction, numbers, infinity, and historical tensions that helped shape modern mathematical rigor.

Moitra explains P versus NP in terms of finding and checking satisfying assignments, then introduces worst-case analysis. The guests consider what this abstraction captures, what it overlooks, and the importance of studying algorithms that exploit the structure of real problems.

Moitra explains the secretary problem and cache management as examples of online algorithms, where future inputs are unknown. He discusses the gap between theoretical guarantees and practical performance, and the challenge of modeling realistic input patterns.

Moitra notes that the reported mathematical results did not explain deep learning or language models. He argues that worst-case difficulty does not capture how natural data behaves, using protein folding to illustrate how real-world problems may have structure that makes them tractable.

Moitra discusses how fine-tuning a language model on apparently unrelated outputs can transfer a hidden preference, such as a preference for owls. He outlines a mathematical account in which concepts overlap in representation space and small effects can accumulate.

The guests discuss how small model behaviors could interact in multi-agent systems and why studying those systems matters as they gain access to digital infrastructure. They distinguish low-stakes, verifiable uses from high-impact decisions and argue for maintaining verification safeguards.

The guests identify P versus NP as a problem they expect to remain difficult and discuss the possibility that many practical instances are easier than worst-case theory suggests. They consider why different classes of satisfiability problems may be easy for different reasons.

The conversation considers mathematical prizes and what they recognize if AI can produce proofs of major results. The guests then discuss using language models to understand unfamiliar papers and potentially accelerate learning across fields.

The guests discuss curiosity and critical judgment as essential skills for learning with AI, especially for younger students. They consider the risks of using tools to bypass difficult work and argue that mastering fundamentals can provide independence even when machines can perform tasks.

Alex advises mathematics PhD students to learn as much difficult, abstract mathematics as they can. The guests discuss different undergraduate uses of AI: checking understanding and studying versus simply obtaining homework answers.

The guests distinguish intelligence from morality and discuss why learning fundamentals, avoiding distractions, and making room for curiosity matter. They reflect on the value of exploration during school and the tension between learning and pressure to produce.

Moitra advises students to find intrinsic reasons for their work rather than relying only on external milestones. He tells a story about college pressure and suggests imagining that one has already achieved the expected career milestone, then choosing what one would genuinely want to do.

The guests discuss meaningful work, uncertainty, and the limits of advice based on successful careers. The conversation closes on combining independent choices with participation in a community, and on family and human relationships as central sources of meaning.