Interactive Theorem Proving with Lean
Guest Lecture, University of Regensburg, Regensburg, Germany
My second repetition of the Regensburg guest lecture, with the AI section rebuilt almost from scratch with all new news.
Talks and presentations
The Lean Module System
Talk, Lean Together 2026, online
Review of my main technical contribution of 2025.
Trusting AI with the Lean Theorem Prover
Invited Talk, NVIDIA, online
Invited talk at the NVIDIA Formal Methods Week.
Trustless AI with the Lean Theorem Prover
Invited Talk, AI4X 2025, Singapore, Singapore
Library Scalability in the Lean Theorem Prover
Talk, NUS, Singapore, Singapore
Talk given at Ilya Sergey’s group.
Interactive Theorem Proving with Lean
Guest Lecture, University of Regensburg, Regensburg, Germany
Guest lecture at the University of Regensburg introducing Lean.
Lean: Past, Present, and Future
Invited Talk, FSCD 2024, Tallinn, Estonia
Talk focusing on how Lean got to the point it is right now and where we’re going with it.
Profiling Tools in Lean
Talk, LMU, Munich, Germany
Presented at Jasmin Blanchette’s group. Presented again at the Prospects of Formal Mathematics program at the Hausdorff Research Institute for Mathematics, Bonn, Germany.
Are We Fast Yet
Conference Talk, Lean Together 2024, online
A summary of how we measure the performance of Lean (on e.g. Mathlib), how it compares to Lean 3, and what we have planned to further improve it.
Scaling Lean to the Next Millions of Lines of Proofs
Keynote, WITS 2024, Braga, Portugal
Review and preview of how we scale Lean to cope with large formalization projects.
Syntax Extensibility in Lean 4
Talk, University of Edinburgh, Edinburgh, Scotland
Talk given during a stay at Tobias Grosser’s group. The last talk of my PhD.
Metaprograms and Proofs: Macros in Lean 4
Conference Talk, RacketCon 2022, Providence, RI, USA
A summary of Lean 4’s macro system with a focus on comparison to Racket’s.
‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language
Conference Talk, ICFP 2024, Ljubljana, Slovenia
Conference talk on our ICFP paper.
An Introduction to the Lean 4 theorem prover and programming language
Tutorial, NASA Formal Methods 2022, online
Lean 4 Tutorial given together with Leonardo de Moura.
Gotta Prove Fast: Building an Ecosystem for Effortless Native Compilation of Tactics
Workshop Talk, WITS 2022, online
Progress report on our native compilation efforts.
Metaprogramming in Lean 4
Tutorial, Lean Together 2021, online
Introduction to Lean 4 metaprogramming given together with Leonardo de Moura.
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Conference Talk, IJCAR 2020, online
Conference talk on our IJCAR paper.
Lean 4: State of the ⋃
Conference Talk, Lean Together 2020, Pittsburgh, PA, USA
Early progress report on Lean 4.
Lean 4: A Guided Preview
Conference Talk, Lean Together 2019, Amsterdam, Netherlands
Even earlier progress report on Lean 4.
An Optimized Object Model for an Interactive Theorem Prover
Talk, ETH Compiler Social, Zurich, Switzerland
Lean 4: Reimplementing Lean in Lean
Internship Report, Microsoft Research, Redmond, WA, USA
Report on my internship under Leonardo de Moura during which we devised the overall design of Lean 4.
A Metaprogramming Framework for Formal Verification
Conference Talk, ICFP 2024, Oxford, UK
Conference talk on our ICFP paper.
Verified Construction of Static Single Assignment Form
Conference Talk, CC 2016, Barcelona, Spain
Conference talk on our CC paper. My first conference talk!