Scott Armstrong joins me to talk about AI and the future of mathematics, including the recent Navier–Stokes developments, what happens to mathematical research if AI can solve major open problems, credit and refereeing, how mathematicians are actually using AI tools, and formalizing serious analysis and PDE in Lean.

Scott Armstrong is a professor of mathematics at NYU, currently on leave and a CNRS Directeur de recherche at Sorbonne University in the Laboratoire Jacques-Louis Lions (LJLL).  
CHAPTERS

00:00 Introduction to Scott Armstrong and episode overview
00:44 Open letter from 25 Fields Medalists
08:58 OpenAI intrigue with Navier–Stokes
13:47 Comments on the Navier–Stokes proof
20:12 OpenAI releasing solutions?
23:26 What do mathematicians work on now?
27:10 The currency of credit and referee requests
34:11 Editorial boards in September 2026
48:53 Using AI tools for math and sanity
52:01 Splitting tasks between different models
57:05 Pros and cons of doing math with AI
01:02:35 Prompting like Levent
01:11:13 De Giorgi–Nash–Moser in Lean
01:22:37 Mathlib
01:30:28 Formalizing Caffarelli–Kohn–Nirenberg in Lean
01:40:42 Leveling up the Lean game with tmux and max

LINKS & RESOURCES

Scott Armstrong
Website: https://www.scottnarmstrong.com/
X: https://x.com/scottnarmstrong

Julia Kempe on The Information Bottleneck
“After Math Falls, What’s Next?”
https://open.spotify.com/episode/5zD9...
After Math Falls, What's Next?  with Julia...

Lean 4 Differential Geometry Library
Ricci flow, Hamilton’s theorem, Perelman’s reduced volume, Hamilton–Ivey pinching, and more:
https://github.com/qinz1yang/differen...

Armstrong & Kempe: De Giorgi–Nash–Moser Regularity in Lean
https://github.com/scottnarmstrong/De...