Uploaded April 2026 | Updated September 2026, 2 weeks ago
2025-26 Allen School Distinguished Lecture Series
Title: What Happens to Software When Proof is Cheap?
Speaker: Mike Dodds (Galois, Inc.)
Date: Thursday, April 16, 2026
Abstract: In July 2025, three AI systems independently achieved gold-medal standard at the International Math Olympiad. One of them, Harmonic's Aristotle, did it by constructing formal proofs in the Lean proof assistant. Six months later, several AIs working together used Lean to solve an open problem posed by Paul Erdős. We may soon live in a strange world where AI is better at math than any human expert.
Lean and tools like it bridge two worlds: mathematicians use them to formalise theorems, but engineers use them to prove that code behaves correctly. This second use, formal verification, has a long history and a few notable successes in cryptography, operating systems, and parser security. But these successes have always been limited by the sheer difficulty of the mathematical reasoning they require.
Now, AI may be changing this picture. If mathematical reasoning is cheap, we could eliminate entire classes of bugs from systems at scale, guarantee that safety-critical code behaves as intended, or verify auto-generated code as fast as it is written. Our need for rigorous verification is growing just as the cost of doing so may be dropping.
The most important software in need of verification may be AI systems themselves. These are growing more capable and more opaque, and we are granting them increasing power over consequential decisions. The same advances making mathematical proof cheaper may also be creating the systems that most urgently need to be proved safe.
Bio: Mike Dodds is a Principal Scientist at Galois, Inc., an employee-owned research company in Portland, OR. Galois builds formal methods and security technologies for clients including DARPA and AWS. Mike's work focuses on making formal verification practical: he led the verification of core cryptographic code in the AWS-LibCrypto library, built reference PDF parsers for the PDF Association, and developed tools for translating legacy C code into Rust. Before Galois, he held academic positions at the University of Cambridge and the University of York, where he worked on separation logic, concurrency, and hardware memory models. He holds a PhD from York.
This video is closed captioned.
2025-26 Allen School Distinguished Lecture Series
Title: What Happens to Software When Proof is Cheap?
Speaker: Mike Dodds (Galois, Inc.)
Date: Thursday, April 16, 2026
Abstract: In July 2025, three AI systems independently achieved gold-medal standard at the International Math Olympiad. One of them, Harmonic's Aristotle, did it by constructing formal proofs in the Lean proof assistant. Six months later, several AIs working together used Lean to solve an open problem posed by Paul Erdős. We may soon live in a strange world where AI is better at math than any human expert.
Lean and tools like it bridge two worlds: mathematicians use them to formalise theorems, but engineers use them to prove that code behaves correctly. This second use, formal verification, has a long history and a few notable successes in cryptography, operating systems, and parser security. But these successes have always been limited by the sheer difficulty of the mathematical reasoning they require.
Now, AI may be changing this picture. If mathematical reasoning is cheap, we could eliminate entire classes of bugs from systems at scale, guarantee that safety-critical code behaves as intended, or verify auto-generated code as fast as it is written. Our need for rigorous verification is growing just as the cost of doing so may be dropping.
The most important software in need of verification may be AI systems themselves. These are growing more capable and more opaque, and we are granting them increasing power over consequential decisions. The same advances making mathematical proof cheaper may also be creating the systems that most urgently need to be proved safe.
Bio: Mike Dodds is a Principal Scientist at Galois, Inc., an employee-owned research company in Portland, OR. Galois builds formal methods and security technologies for clients including DARPA and AWS. Mike's work focuses on making formal verification practical: he led the verification of core cryptographic code in the AWS-LibCrypto library, built reference PDF parsers for the PDF Association, and developed tools for translating legacy C code into Rust. Before Galois, he held academic positions at the University of Cambridge and the University of York, where he worked on separation logic, concurrency, and hardware memory models. He holds a PhD from York.
This video is closed captioned.
![[Audio Descriptions] I Am CSE: Melanie Sclar](https://i.ytimg.com/vi/oXbk5FnpUnE/mqdefault.jpg "[Audio Descriptions] I Am CSE: Melanie Sclar
Melanie Sclar, a graduate student in the Allen School’s Natural Language Processing group, explains her work to advance the ability of large language models to engage in human-like reasoning known as “theory of mind” and why the Allen School is a big destination for researchers in AI.
This video is closed captioned.
A version of this video without audio descriptions is available here: https://youtu.be/OGQzgUVKwb0.")
![[ASL] Toward Total Scene Understanding for Autonomous Driving—Drago Anguelov (Waymo)](https://i.ytimg.com/vi/pK5ChzMsfE0/mqdefault.jpg "[ASL] Toward Total Scene Understanding for Autonomous Driving—Drago Anguelov (Waymo)
Ben Taskar Distinguished Memorial Lecture
Title: Toward Total Scene Understanding for Autonomous Driving
Speaker: Drago Anguelov (Waymo)
Host: Anat Caspi
Date: January 25, 2024
Abstract: Machine learning has proven to be a key ingredient in building a performant and scalable Autonomous Vehicle stack, spanning key capabilities such as perception, behavior prediction, planning and simulation and evaluation. I will describe recent Waymo research on performant ML models and architectures that help us handle the variety and complexity of real world environments. I will also discuss how progress in building Autonomous Driving agents can impact people with disabilities and cover some current open questions about how to further enhance embodied AI agent capabilities with ML.
Bio: Drago joined Waymo in 2018 to lead the Research team, which focuses on pushing the state of the art in autonomous driving using machine learning. Earlier in his career he spent eight years at Google; first working on 3D vision and pose estimation for StreetView, and later leading a research team which developed computer vision systems for annotating Google Photos. The team also invented popular methods such as the Inception neural network architecture, and the SSD detector, which helped win the Imagenet 2014 Classification and Detection challenges. Prior to joining Waymo, Drago led the 3D Perception team at Zoox.
This video is closed captioned.
A version of this video without ASL interpretation is available here: https://youtu.be/zCJO7ONdPZM.")
