Topic: Lean

Ken Ono surveys how AI systems contribute to mathematical discovery, research-level reasoning and formal verification. Examples include AI-guided searches, progress on longstanding problems and formalization in Lean. The talk also examines reliability, attribution, unequal access, education and the future role of mathematicians. It argues for using AI to extend exploration while retaining mathematical judgment and strengthening trust through machine-checkable proofs.

Carina Hong discusses building systems for mathematical reasoning and machine-verifiable proofs. The conversation explores Lean, the scarcity of formal mathematical training data, and translating natural-language arguments into formal statements. It also examines conjecture-and-proof self-play and applications of formal verification to software and hardware.

Kevin Buzzard of Imperial College London joins Steven Strogatz to discuss Lean, formal proof assistants and the effort to encode mathematical knowledge in a computer-readable library. They explore how computers verify difficult arguments, the distinction between Lean and its mathematical library, the formalization of work by Peter Scholze and Dustin Clausen, and the prospects and limits of computers creating new mathematics.