Strachey Lecture: The Lean Theorem Prover/Will computers prove theorems?

Speaker
Professor Leo de Moura, Professor Kevin Buzzard
Event date
Event time
14:30
Venue
Mathematical Institute, Andrew Wiles Building
Radcliffe Observatory Quarter
Oxford
OX2 6GG
Venue details

Lecture Theatre 1

Event type
Lectures and seminars
Event cost
Free
Disabled access?
Yes
Booking required
Required

This Strachey Lecture is a double bill taking place from 2:30pm-4:30pm (followed by coffee).
Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI
Kevin Buzzard: Will Computers prove theorems?

Abstract of Leo De Moura's Talk:
How can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate.
In this talk, I will highlight how Lean is being used to tackle challenging problems in mathematics, software verification, and AI research that depends on formally sound reasoning. I will also introduce the Lean Focused Research Organization (FRO), a non-profit dedicated to expanding Lean’s capabilities and community. By showcasing real-world examples, ranging from advanced research projects to industry-driven applications, I illustrate how Lean empowers us to innovate in a more reliable, transparent, and truly collective manner.

Abstract of Kevin Buzzard's Talk:
Will computers one day replace human mathematicians? Is this just around the corner, or decades away? Can neural networks spot patterns which humans have missed? Currently, language models are great for brainstorming big ideas but are very poor when it comes to details. Can integrating a language model with a theorem prover like Lean solve these problems? Is the modern mathematical literature riddled with errors, and is it feasible to hope that a machine might find and even fix them? Is it possible to teach a computer the proof of Fermat's Last Theorem? And what do mathematicians make of all this? I'll talk about how modern developments in AI and theorem provers are beginning to affect mathematics.