What Happens to Software When Proof is Cheap?
Mike Dodds (Galois, Inc.)
Distinguished Lecture Series
Thursday, April 16, 2026, 3:30 pm
Gates Center (CSE2), G20 | Amazon Auditorium
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 lecture will be recorded and streamed live on the Allen School's YouTube channel (https://www.youtube.com/@uwcse), unless otherwise noted. The link will be available on that page one hour prior to the event.
The University of Washington is committed to providing access, equal opportunity and reasonable accommodation in its services, programs, activities, education and employment for individuals with disabilities. Live captioning will be provided for this event. To request disability accommodation such as ASL interpretation, contact the Disability Services Office at least ten days in advance of the event at: (206) 543-6450/V, (206) 543-6452/TTY, (206) 685-7264 (FAX), or email at dso@u.washington.edu.