Publications
This is a list of papers and presentations about Lean by the Lean developers. For further publications about Lean, the mathlib library, and other formalizations in Lean, please also see the Lean community website.
Papers
- An Extensible Theorem Proving Frontend PhD Thesis, Karlsruhe Institute of Technology, Germany, 2023
- ‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl) 27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022), Ljubljana, Slovenia, 2022
- The Lean 4 Theorem Prover and Programming Language 28th International Conference on Automated Deduction (CADE-28), Pittsburgh, USA, 2021
- Tabled Typeclass Resolution draft, 2020
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, 2020
- Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming The 31st symposium on Implementation and Application of Functional Languages (IFL 2019), Singapore, 2019
- A Metaprogramming Framework for Formal Verification. 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017), Oxford, UK, 2017
- Developing Bug-Free Machine Learning Systems With Formal Mathematics. Thirty-fourth International Conference on Machine Learning (ICML) 2017
- Congruence Closure in Intensional Type Theory International Joint Conference on Automated Reasoning (IJCAR), Coimbra, Portugal, 2016
- The Lean Theorem Prover. 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015
- Elaboration in Dependent Type Theory. A description of the elaborator used in Lean 2 only
Presentations
-
Lean Together 2024, January 2024
-
Sebastian Ullrich: Are We Fast Yet.
-
-
Machine-Checked Proofs and the Rise of Formal Methods in Mathematics, video, Simons Institute, Berkeley, October 2023.
-
Lean 4: an extensible proof assistant and programming language, ITP Summer School, September 2023.
-
Lean 4: Empowering the Formal Mathematics Revolution and Beyond, Topos Institute, September 2023.
-
The Lean Focused Research Organization, Lean for the Curious Mathematician 2023, September 2023.
-
Scaling Lean to the Next Millions of Lines of Proofs, WITS 2023, August 2023.
-
Syntax Extensibility in Lean 4, University of Edinburgh, June 2023.
-
Metaprograms and Proofs: Macros in Lean 4, RacketCon 2022, October 2022.
-
‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl) [video], ICFP 2022, September 2022.
-
Lean 4, Lean for the Curious Mathematician, [video], July 2022.
-
An Introduction to the Lean 4 theorem prover and programming language, NASA Formal Methods Symposium, May 2022.
-
Gotta Prove Fast: Building an Ecosystem for Effortless Native Compilation of Tactics [video], Workshop on the Implementation of Type Systems 2022, January 2022.
-
Metaprogramming in Lean 4 [slides pt. 1] [slides pt. 2] [video] [video cont.], Lean Together 2021, January 2021.
-
An overview of Lean 4 [slides pt. 1] [slides pt. 2] [video], Lean Together 2021, January 2021.
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages [video], IJCAR 2020, July 2020.
-
Lean in Lean, ACL2 workshop, May 2020.
-
Lean 4: State of the ⋃ [video], Formal Methods in Mathematics / Lean Together 2020, Pittsburgh, January 2020.
-
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming, IFL 2019, Singapore, September 2019.
-
Lean 4: a guided preview, Lean Together 2019, Amsterdam, January 2019.
-
An optimized object model for an interactive theorem prover [video], ETH Compiler Social, Zurich, December 2018.
-
Lean 4: reimplementing Lean in Lean, internship report, Redmond, October 2018.
-
Lean: past, present and future, Galois Inc., Oregon, August 2018.
-
Efficient verification and metaprogramming in Lean, 22nd International Symposium on Formal Methods, Oxford, July 2018
-
White-box automation, International Conference on Interactive Theorem Proving, Brasilia, September 2017
-
From Z3 to Lean, The Alan Turing Institute, London, July 2017
-
Metaprogramming with Dependent Type Theory, Issac Newton Institute for Mathematical Sciences, Cambridge, July 2017
-
The Lean Theorem Prover, POPL'17, Paris, January 2017
-
Formal Methods in Mathematics and the Lean Theorem Prover, CSLI, Stanford, January 2017
-
The Lean Theorem Prover, ICTAC'16, Taipei, Taiwan, October 2106
-
The Lean Theorem Prover and Automation, CPP'16, St. Petersburg, Florida, January 2016
-
Type Theory and Practical Foundations (with examples in Lean), Fields Institute, Toronto, February 2016
-
The Lean Theorem Prover (CADE system description) CADE'25, Berlin, Germany, August 2015
-
Lean CADE Tutorial, CADE'25, Berlin, Germany, August 2015
-
The Lean Theorem Prover, CICM, Washington D.C., July 2015
-
The Lean Theorem Prover, PL(X) meeting at Microsoft Research, February 2015