TT25 Strachey Lecture

Profs. Leo De Moura & Kevin Buzzard ( Amazon Web Services & Imperial College London )

6May
15:00 6th May 2025
TBC

Abstract & title TBC

Speaker bio

https://leodemoura.github.io/about.html

Leo De Moura: Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.

Awards

(2010) Haifa Verification Conference Award.
(2014) “The most influential tool paper in the first 20 years of TACAS” for the paper: Z3: An Efficient SMT Solver. (TACAS conference)
(2015) Programming Languages Software Award for Z3.
(2017) Skolem Award for the paper “Efficient E-Matching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field.
(2018) Test of time award for the paper: Z3: An Efficient SMT Solver. (ETAPS conference)
(2019) Herbrand award for numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs.
(2021) CAV Award for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).
(2021) Distinguished paper award at PLDI for the paper “Perceus: Garbage Free Reference Counting with Reuse”.

https://www.imperial.ac.uk/people/k.buzzard

Kevin Buzzard: My background is in algebraic number theory. Currently I work in the area of formal proof verification. I believe that within my lifetime, computers will be able to help human mathematicians to create proofs, and I am actively trying to accelerate this process. Three ways I do this:

* I help to build a database of modern mathematical theorems and definitions;

* I teach mathematics undergraduates how to use the software which can read the database;

* From October 2024 I will be leading a project to formalise a 21st century proof of Fermat's Last Theorem.

If you are a mathematician (or a future mathematician) interested in starting to learn about how to prove theorems using computers, you could try the natural number game! Want some more advanced mathematics? Read about how Commelin, Massot and I told a computer what a perfectoid space was!

Some of my recent talks:

* The 2023 Bernays Lectures, ETH Zurich.

* The 2022 Plücker lectures, University of Bonn

* My plenary lecture at the 2022 International Congress of Mathematics.

* Will Computers Outsmart Mathematicians? (2021 talk for a general audience at Gresham College).