Papers

“The Lean Theorem Prover.” PDF
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer,
25th International Conference on Automated Deduction (CADE25), Berlin, Germany, 2015. 
“A Metaprogramming Framework for Formal Verification.” PDF
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura,
22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017), Oxford, UK, 2017. 
“Developing BugFree Machine Learning Systems With Formal Mathematics.” Source code
Daniel Selsam, Percy Liang, David L. Dill, Thirtyfourth International Conference on Machine Learning (ICML) 2017. 
“Congruence Closure in Intensional Type Theory.” PDF
Daniel Selsam and Leonardo de Moura,
International Joint Conference on Automated Reasoning (IJCAR), Coimbra, Portugal, 2016. 
“Elaboration in Dependent Type Theory.” PDF
Leonardo de Moura, Jeremy Avigad, Soonho Kong and Cody Roux
A description of the elaborator used in Lean 2 only.
Presentations

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
Formalizations

“Constructing the Propositional Truncation using Nonrecursive HITs”. arXiv, code
Floris van Doorn. Certified Proofs and Programs (CPP), 2016 
“The CayleyDickson Construction in Homotopy Type Theory”. arXiv
Ulrik Buchholtz and Egbert Rijke
Theses

Formalization of nonabelian topology for homotopy type theory. PDF, code
Jakob von Raumer, MS thesis, Karlruhe Institute of Technology, 2015. 
Simple Verification of Rust Programs via Functional Purification. PDF, code
Sebastian Ullrich, MS thesis, Karlruhe Institute of Technology, 2016.
Courses
 Logic and Proof. An introductory course for undergraduates.
online tutorial,
pdf
Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn.