Papers
Papers about Lean
- Daniel Selsam, Simon Hudon, Leonardo de 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 de 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
- Jannis Limperg, A Novice-Friendly Induction Tactic for Lean. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021 lean3
- Anne Baanen, A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, 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
- Anne Baanen, Sander Dahmen, Ashvni Narayanan, Filippo Nuccio, A formalization of Dedekind domains and class groups of global fields. 2021 (website) lean3
- Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Mir, Scott Morrison, Schemes in Lean. 2021 lean3
- Johan Commelin, Robert Lewis, Formalizing the Ring of Witt Vectors. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021 (website) lean3
- Alena Gusakov, Bhavik Mehta, Kyle Miller, Formalizing Hall's Marriage Theorem in Lean. 2021 lean3
- Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan, A Formal Proof of PAC Learnability for Decision Stumps. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021 lean3
- 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.