Papers

Papers about Lean

• Daniel Selsam, Simon Hudon, Leonardo Moura, Sealing Pointer-Based Optimizations behind Pure Functions Proc. ACM Program. Lang., 2020 lean4
• Daniel Selsam, Sebastian Ullrich, Leonardo de Moura, Tabled Typeclass Resolution 2020 lean4
• Sebastian Ullrich, Leonardo Moura, Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, 2020 lean4
• Mario Carneiro, The Type Theory of Lean 2019 lean3
• Marc Huisinga, Formally Verified Insertion of Reference Counting Instructions 2019 (website) lean4
• Sebastian Ullrich, Leonardo de Moura, Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming 2019 lean4
• Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura, A metaprogramming framework for formal verification PACMPL, 2017 lean3
• Daniel Selsam, Leonardo de Moura, Congruence Closure in Intensional Type Theory Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, 2016 lean2
• Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux, Elaboration in Dependent Type Theory 2015 lean2
• Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer, The Lean Theorem Prover (System Description) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 2015 lean2

Papers about mathlib

• Anne Baanen, A Lean tactic for normalising ring expressions with exponents 2020 lean3
• Robert Lewis, Paul-Nicolas Madelaine, Simplifying Casts and Coercions Practical Aspects of Automated Reasoning, PAAR 2020, 2020 lean3
• Robert Lewis, Minchao Wu, A bi-directional extensible interface between Lean and Mathematica 2020 (website) lean3
• The mathlib community, The Lean mathematical library Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, 2020 (website) lean3
• Floris van Doorn, Gabriel Ebner, Robert Lewis, Maintaining a Library of Formal Mathematics Intelligent Computer Mathematics, CICM 2020, 2020 lean3
• Paul-Nicolas Madelaine, Arithmetic and Casting in Lean 2019 lean3
• Robert Lewis, An Extensible Ad Hoc Interface between Lean and Mathematica Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017, 2017 (website) lean3

Formalization papers using Lean

• Kevin Buzzard, Johan Commelin, Patrick Massot, Formalising perfectoid spaces Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, 2020 (website) lean3
• Jesse Han, Floris van Doorn, A formal proof of the independence of the continuum hypothesis Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, 2020 (website) lean3
• Mario Carneiro, Formalizing Computability Theory via Partial Recursive Functions 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 2019 (website) lean3
• Sander Dahmen, Johannes Hölzl, Robert Lewis, Formalizing the Solution to the Cap Set Problem 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 2019 (website) lean3
• Ramon Mir, Schemes in Lean 2019 (website) lean3
• Jesse Han, Floris van Doorn, A Formalization of Forcing and the Unprovability of the Continuum Hypothesis 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 2019 lean3
• Robert Lewis, A formal proof of Hensel's lemma over the p-adic integers Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019 lean3
• Neil Strickland, Nicola Bellumat, Iterated chromatic localisation 2019 (website) lean3
• Floris van Doorn, Constructing the propositional truncation using non-recursive HITs Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, 2016 lean2
• Sebastian Ullrich, Simple Verification of Rust Programs via Functional Purification 2016 (website) lean2
• Jakob von Raumer, Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, 2016 lean2
• Jakob von Raumer, Formalization of Non-Abelian Topology for Homotopy Type Theory 2015 (website) lean2

You can find all those papers and more in lean.bib.