The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:
"Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean
Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.
Watch Leo's lecture here: https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai
"Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College
Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.
Watch Kevin's lecture here: https://podcasts.ox.ac.uk/will-computers-prove-theorems