Papers

Papers about Lean

• Wojciech Nawrocki, Edward Ayers, Gabriel Ebner, An Extensible User Interface for Lean 4. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean4
• Sebastian Ullrich, Leonardo Moura, 'do' unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 2022 lean4
• Leonardo Moura, Sebastian Ullrich, The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, 2021 lean4
• 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, Asta From, Aesop: White-Box Best-First Proof Search for Lean. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean4
• Anne Baanen, Use and Abuse of Instance Parameters in the Lean Mathematical Library. 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 lean3
• Robert Lewis, Minchao Wu, A bi-directional extensible interface between Lean and Mathematica. Journal of Automated Reasoning, 2022 (website) lean3
• Alexander Best, Automatically Generalizing Theorems Using Typeclasses. 2021 lean3
• Jannis Limperg, A Novice-Friendly Induction Tactic for Lean. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021 lean3
• Eric Wieser, Scalar actions in Lean's mathlib. 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
• 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

• Riccardo Brasca, Christopher Birkbeck, Eric Boidi, Alex Best, Ruben De Velde, Andrew Yang, A complete formalization of Fermat's Last Theorem for regular primes in Lean. Annals of Formalized Mathematics, 2025 lean4
• David Loeffler, Michael Stoll, Formalizing zeta and L-functions in Lean. Annals of Formalized Mathematics, 2025 lean4
• Salvatore Mercuri, Formalising the local compactness of the adele ring. Annals of Formalized Mathematics, 2025 lean4
• Joël Riou, Formalization of derived categories in Lean/mathlib. Annals of Formalized Mathematics, 2025 lean4
• Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Nuccio Mortarino Majno di Capriglio, Adam Topaz, Categorical foundations of formalized condensed mathematics. The Journal of Symbolic Logic, 2024 lean4
• Dagur Asgeirsson, Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Henning Basold, Peter Bruin, Dominique Lawson, The Directed Van Kampen Theorem in Lean. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, Tobias Grosser, Verifying Peephole Rewriting in SSA Compiler IRs. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad, Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• María Frutos-Fernández, Filippo Nuccio Mortarino Majno di Capriglio, A Formalization of Complete Discrete Valuation Rings and Local Fields. Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '24), 2024 lean3
• Sam Ezeh, Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Patrick Massot, Teaching Mathematics Using Lean and Controlled Natural Language. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Kai Obendrauf, Anne Baanen, Patrick Koopmann, Vera Stebletsova, Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, Marijn Heule, Formal Verification of the Empty Hexagon Number. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Floris Doorn, Heather Macbeth, Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 lean4
• Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman, A Proof-Producing Compiler for Blockchain Applications. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• David Angdinata, Junyan Xu, An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Anne Baanen, Alex Best, Nirvana Coppola, Sander Dahmen, Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean3
• Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Fermat’s Last Theorem for Regular Primes. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Joshua Clune, A Formalized Reduction of Keller's Conjecture. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean3
• María Frutos-Fernández, Formalizing Norm Extensions and Applications to Number Theory. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Floris Doorn, Patrick Massot, Oliver Nash, Formalising the h-Principle and Sphere Eversion. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean3
• Martin Dvorak, Jasmin Blanchette, Closure Properties of General Grammars – Formally Verified. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Amelia Livingston, Group Cohomology in the Lean Community Library. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Bhavik Mehta, Formalising Sharkovsky's Theorem (Proof Pearl). Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean3
• Oliver Nash, A Formalisation of Gallagher’s Ergodic Theorem. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak, A Pretty Expressive Printer. Proc. ACM Program. Lang., 2023 lean4
• Eric Wieser, Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies. Intelligent Computer Mathematics, 2023 lean3 lean4
• Kexing Ying, Rémy Degenne, A Formalization of Doob's Martingale Convergence Theorems in mathlib. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, 2023 lean3
• Jujian Zhang, Formalising the Proj Construction in Lean. 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 lean3
• Anne Baanen, Sander Dahmen, Ashvni Narayanan, Filippo Nuccio Mortarino Majno di Capriglio, A formalization of Dedekind domains and class groups of global fields. J. Automat. Reason., 2022 lean3
• Thomas Browning, Patrick Lutz, Formalizing Galois Theory. Experimental Mathematics, 2022 lean3
• Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Mir, Scott Morrison, Schemes in Lean. Exp. Math., 2022 lean3
• María Frutos-Fernández, Formalizing the Ring of Adèles of a Global Field. 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 lean3
• Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean. 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 lean3
• Frédéric Dupuis, Robert Lewis, Heather Macbeth, Formalized functional analysis with semilinear maps. 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 lean3
• Sébastien Gouëzel, A Formalization of the Change of Variables Formula for Integrals in mathlib. Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, 2022 lean3
• Bjørn Kjos-Hanssen, Saroj Niraula, Soowhan Yoon, A parametrized family of Tversky metrics connecting the Jaccard distance to an analogue of the normalized information distance. LFCS: Logical foundations of computer science, 2022 lean3
• Yury Kudryashov, Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 lean3
• Bhavik Mehta, Formalising the Kruskal-Katona Theorem in Lean. Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, 2022 lean3
• Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak, A Formal Foundation for Symbolic Evaluation with Merging. Proc. ACM Program. Lang., 2022 lean3
• Eric Wieser, Utensil Song, Formalizing Geometric Algebra in Lean. Advances in Applied Clifford Algebras, 2022 (website) lean3
• Eric Wieser, Jujian Zhang, Graded Rings in Lean's Dependent Type Theory. Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, 2022 lean3
• Anne Baanen, Sander Dahmen, Ashvni Narayanan, Filippo Nuccio Mortarino Majno di Capriglio, A Formalization of Dedekind Domains an Class Groups of Global Fields. 12th International Conference on Interactive Theorem Proving (ITP 2021), 2021 lean3
• Anthony Bordg, Nicolò Cavalleri, Elements of Differential Geometry in Lean: A Report for Mathematicians. 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
• Floris van Doorn, Formalized Haar Measure. 12th International Conference on Interactive Theorem Proving (ITP 2021), 2021 lean3
• Sébastien Gouëzel, Formalizing the Gromov-Hausdorff space. 2021 lean3
• Alena Gusakov, Bhavik Mehta, Kyle Miller, Formalizing Hall's Marriage Theorem in Lean. 2021 lean3
• Yury Kudryashov, Formalizing Rotation Number and Its Properties 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.