Joint Colloquium: Leo de Moura, “Machine‑Checked Mathematics and AI Collaboration” – 5/8, 3:30 p.m.

Joint Colloquium: Departments of Mathematics, Computer Science, and Electrical & Computer Engineering

Lean: Machine‑Checked Mathematics and AI Collaboration

Speaker: Leo de Moura, Senior Principal Applied Scientist, AWS Chief Architect & Co‑Founder of the Lean FRO, a non-profit organization dedicated to the development of the Lean theorem prover and programming language

Date: Friday, May 8, 2026 Time: 3:30–4:30 PM Location: ECE 105

Abstract

Lean is a proof assistant and programming language designed to make formal verification practical. In this talk, Leo de Moura will describe how Lean works, what it can do today, and where it is going. The core idea is simple: every mathematical claim and every program can be checked by a machine. This changes what collaboration looks like: between mathematicians, between engineers, and increasingly between humans and AI systems. When a proof is machine-checked, you do not need to trust the author. You just check it. Moura will discuss recent work on proof automation and AI-assisted formalization, including experiments in which multi-agent AI systems work autonomously on Lean tasks. Moura will also describe Lean FRO, a nonprofit building Lean as long-term open infrastructure for mathematics and verified software.

Reception

A social reception will follow the talk. **by invite only**

Time: 4:30–6:00 PM Location: ECE 269