After Math Falls, What's Next? with Julia Kempe (NYU/Meta)

Julia Kempe of NYU's Center for Data Science and Meta FAIR discusses why verifiable domains such as mathematics may be overtaken by AI the way Go was. With formal verification in Lean and the Mathlib library, language-model agents can generate and check proofs at scale, and she argues that automated mathematical discovery is closer than many mathematicians expect. The episode covers progress on Erdős problems, what is still missing for harder areas such as analysis and physics, and how synthetic data, curation and verification fit together.