Topic: AI-generated proofs

Recorded live at the International Congress of Mathematicians in Philadelphia, this episode brings hosts Janna Levin and Steven Strogatz together with Akshay Venkatesh, Ravi Vakil and Alex Kontorovich. They examine what recent AI-generated proofs demonstrate, how machine assistance may change mathematical research, and what proof, creativity, understanding and storytelling contribute to the discipline. The recording took place on 26 July 2026; Quanta published the episode on 3 September 2026.

Leonardo de Moura explains how the Lean proof assistant supports interactive mathematical proofs and mechanically verified software. The lecture discusses extensibility, collaborative formalisation and Lean’s mathematical library, with examples from the Liquid Tensor Experiment, mathematics education and the verification challenges associated with AI-generated proofs.