Bibliography

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Every work cited on the pages of this edition, listed once, with the pages that cite it in reading order. There are 277: 86 papers and books; 114 items of Lean documentation and source, 52 of them parts of the reference manual; 64 project pages and announcements; and 13 press articles and encyclopedia entries.

Two citations are taken to be one work when they share a DOI, an arXiv number or a web address. A preprint and its published version are listed apart when the pages cite them apart, and so is each version of a document that changes with Lean: a chapter of the reference manual cited in its edition for Lean 4.34.0 on some pages and for Lean 4.35.0 on others appears twice, once under each address.

Where pages cite one work in different forms, the form given here is the fullest, and a note says what differs when it is more than punctuation, capitals or the sections a page names. The 19 works that were not read, or were read only in part, are marked; the sources page says what each one carries and what carries it instead.

Papers and books

Andreas Abel and Thierry Coquand, "Failure of normalization in impredicative type theory with proof-irrelevant propositional equality", Logical Methods in Computer Science 16(2) (2020), paper 14. https://doi.org/10.23638/LMCS-16(2:14)2020 Cited on Universes and Prop, Definitional equality, Proof irrelevance and subsingleton elimination, Consistency and the metatheory.
Anne Baanen, "Use and Abuse of Instance Parameters in the Lean Mathematical Library", in 13th International Conference on Interactive Theorem Proving (ITP 2022), Leibniz International Proceedings in Informatics 237, Schloss Dagstuhl, 2022, pp. 4:1–4:20. doi:10.4230/LIPIcs.ITP.2022.4 Cited on Type classes and instance resolution.
Anne Baanen, Matthew R. Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang and Damiano Testa, "Growing Mathlib: maintenance of a large scale mathematical library", arXiv:2508.21593, version 2, 7 October 2025; to appear at the Conference on Intelligent Computer Mathematics (CICM) 2025. arxiv.org/abs/2508.21593 Cited on Checking a proof again later, A library of mathematics.
Henk Barendregt and Freek Wiedijk, "The challenge of computer mathematics", Philosophical Transactions of the Royal Society A 363 (1835), 2005, pp. 2351–2375. doi:10.1098/rsta.2005.1650. Author's copy: https://www.cs.ru.nl/~freek/pubs/rspaper.pdf Cited on The small trusted core, Automath, Further reading.
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, et al., "A blueprint for the formalization of Carleson's theorem on convergence of Fourier series", arXiv:2405.06423, May 2024 (revised 6 August 2025). https://arxiv.org/abs/2405.06423 Cited on Research mathematics.
Maxwell P. Bobbin, Colin Jones, John Velkey and Tyler R. Josephson, "Formalizing dimensional analysis using the Lean theorem prover", arXiv:2509.13142, 16 September 2025. arxiv.org/abs/2509.13142 Cited on Lean and physics.
Matthew Bolan, Joachim Breitner, Jose Brox, et al. (34 authors, including Terence Tao), "The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale", arXiv:2512.07087, December 2025 (revised 16 December 2025). https://arxiv.org/abs/2512.07087 Cited on Research mathematics, The polynomial Freiman-Ruzsa conjecture, The equational theories project, Machine learning and theorem proving.
Ana Bove, Peter Dybjer and Ulf Norell, "A brief overview of Agda – a functional language with dependent types", in Theorem Proving in Higher Order Logics (TPHOLs 2009), Lecture Notes in Computer Science 5674, Springer, 2009, pp. 73–78. doi:10.1007/978-3-642-03359-9_6 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Martin-Löf type theory.
N. G. de Bruijn, "The mathematical language AUTOMATH, its usage, and some of its extensions", in Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer, 1970, pp. 29–61. doi:10.1007/BFb0060623. Scan in the Automath Archive: https://automath.win.tue.nl/archive/pdf/aut002.pdf Cited on Automath.
N. G. de Bruijn, "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem", Indagationes Mathematicae 34 (= Proceedings KNAW A 75), 1972, pp. 381–392. doi:10.1016/1385-7258(72)90034-0. Reprint from Selected Papers on Automath in the Eindhoven repository: https://alexandria.tue.nl/repository/freearticles/597619.pdf Cited on Terms, types and judgments, Automath.^[1]
N. G. de Bruijn, "A survey of the project Automath", in J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 579–606; reprinted in Nederpelt, Geuvers and de Vrijer (eds.), Selected Papers on Automath (1994), pp. 141–161. Scan in the Automath Archive: https://automath.win.tue.nl/archive/pdf/aut072.pdf Cited on Automath.
Kevin Buzzard, Johan Commelin and Patrick Massot, "Formalising perfectoid spaces", in CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020, pp. 299–312. doi:10.1145/3372885.3373830. arXiv:1910.12320 Cited on Research mathematics, Teaching with Lean.
Mario Carneiro, The Type Theory of Lean, MSc thesis, Carnegie Mellon University, 2019. https://github.com/digama0/lean-type-theory/releases/tag/v1.0 Cited on Terms, types and judgments, Dependent function types, Universes and Prop, Inductive types and recursors, Definitional equality, Propositional equality, Quotient types, The three axioms, Proof irrelevance and subsingleton elimination, Consistency and the metatheory, The Calculus of Constructions, Further reading.^[2]
Mario Carneiro, "Lean4Lean: Verifying a Typechecker for Lean, in Lean", arXiv:2403.14064, version 3, 14 September 2025. arxiv.org/abs/2403.14064 Cited on What has to be trusted, Checking a proof again later, Consistency and the metatheory.^[3]
Mario Carneiro, "Lean4Lean: Verifying a Typechecker for Lean, in Lean", in 31st International Conference on Types for Proofs and Programs (TYPES 2025), Leibniz International Proceedings in Informatics 384, Schloss Dagstuhl, 2026, pp. 2:1–2:23. doi:10.4230/LIPIcs.TYPES.2025.2; preprint arXiv:2403.14064. Cited on Two kinds of equality, Terms, types and judgments, Inductive types and recursors, Definitional equality, Proof export and independent checkers, Further reading.^[4]
Alonzo Church, "A note on the Entscheidungsproblem", Journal of Symbolic Logic 1 (1936), pp. 40–41. doi:10.2307/2269326 Cited on Automation and its limits.
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki and S. F. Smith, Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986. ISBN 0-13-451832-2. Catalogue record: https://openlibrary.org/books/OL2715187M Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Martin-Löf type theory.
Thierry Coquand and Gérard Huet, "Constructions: a higher order proof system for mechanizing mathematics", in EUROCAL '85, Lecture Notes in Computer Science 203, Springer, 1985, pp. 151–184. doi:10.1007/3-540-15983-5_13 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on The Calculus of Constructions.
Thierry Coquand and Gérard Huet, "The calculus of constructions", INRIA Research Report RR-0530, May 1986. https://inria.hal.science/inria-00076024 Cited on The Calculus of Constructions.
Thierry Coquand and Gérard Huet, "The calculus of constructions", Information and Computation 76(2–3), 1988, pp. 95–120. https://doi.org/10.1016/0890-5401(88)90005-3 Cited on Universes and Prop, The Calculus of Constructions.^[5]
Thierry Coquand and Christine Paulin, "Inductively defined types", in P. Martin-Löf and G. Mints (eds.), COLOG-88, Lecture Notes in Computer Science 417, Springer, 1990, pp. 50–66. doi:10.1007/3-540-52335-9_47 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on The Calculus of Constructions.
H. B. Curry, "Functionality in combinatory logic", Proceedings of the National Academy of Sciences 20 (11), 1934, pp. 584–590. doi:10.1073/pnas.20.11.584 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Propositions as types.
Joseph W. Cutler, Craig Disselkoen, Aaron Eline, et al., "Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization", Proceedings of the ACM on Programming Languages 8 (OOPSLA1), 2024, pp. 670–697. doi:10.1145/3649835 Cited on Software verification.
Radu Diaconescu, "Axiom of choice and complementation", Proceedings of the American Mathematical Society 51 (1), 1975, pp. 176–178. doi:10.1090/S0002-9939-1975-0373893-X Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on What the axioms are, Classical logic from choice.
Craig Disselkoen, Aaron Eline, Shaobo He, et al., "How We Built Cedar: A Verification-Guided Approach", in Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE Companion '24), 2024. doi:10.1145/3663529.3663854. arXiv:2407.01688 Cited on Software verification.
Floris van Doorn, Jakob von Raumer and Ulrik Buchholtz, "Homotopy type theory in Lean", in Interactive Theorem Proving (ITP 2017), Lecture Notes in Computer Science 10499, Springer, 2017, pp. 479–495. doi:10.1007/978-3-319-66107-0_30. Preprint: https://arxiv.org/abs/1704.06781 Cited on Lean 1 to Lean 3.
Peter Dybjer, "Inductive families", Formal Aspects of Computing 6(4), 1994, pp. 440–465. https://doi.org/10.1007/BF01211308 Cited on Inductive types and recursors.
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad and Leonardo de Moura, "A metaprogramming framework for formal verification", Proceedings of the ACM on Programming Languages 1 (ICFP), article 34, 2017. doi:10.1145/3110278. Author's copy: https://lean-lang.org/papers/tactic.pdf Cited on LCF and the tactic idea, The Calculus of Constructions, Lean 1 to Lean 3, Further reading.
Herman Geuvers, "Proof assistants: history, ideas and future", Sādhanā 34 (1), 2009, pp. 3–25. doi:10.1007/s12046-009-0001-5 Cited on What a proof assistant does, Checking instead of convincing.
Herman Geuvers and Rob Nederpelt, "Characteristics of de Bruijn's early proof checker Automath", Fundamenta Informaticae 185 (4), 2022, pp. 313–336. doi:10.3233/FI-222112. Preprint: https://arxiv.org/abs/2203.01173 Cited on Automath.
Kurt Gödel, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatshefte für Mathematik und Physik 38 (1931), 173–198. https://doi.org/10.1007/BF01700692 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Automation and its limits, Consistency and the metatheory.
Warren D. Goldfarb, "The undecidability of the second-order unification problem", Theoretical Computer Science 13(2), 1981, pp. 225–230. doi:10.1016/0304-3975(81)90040-2. Not consulted directly; the result is stated, with this citation, in the introduction of Miller 1991. Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Metavariables and unification.
Nicolas D. Goodman and John Myhill, "Choice implies excluded middle", Zeitschrift für mathematische Logik und Grundlagen der Mathematik 24 (1978), 461. https://doi.org/10.1002/malq.19780242514 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Classical logic from choice.
M. Gordon, R. Milner, L. Morris, M. Newey and C. Wadsworth, "A metalanguage for interactive proof in LCF", in Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '78), ACM, 1978, pp. 119–130. doi:10.1145/512760.512773 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on LCF and the tactic idea.
Michael J. Gordon, Robin Milner and Christopher P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science 78, Springer, 1979. doi:10.1007/3-540-09724-4 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on LCF and the tactic idea.
Michael J. C. Gordon, "From LCF to HOL: a short history", in Gordon Plotkin, Colin Stirling and Mads Tofte (eds), Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000. https://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html Cited on Tactics, Automation and its limits, LCF and the tactic idea, Martin-Löf type theory, Further reading.^[6]
W. T. Gowers, Ben Green, Freddie Manners and Terence Tao, "On a conjecture of Marton", arXiv:2311.05762, 9 November 2023 (revised 12 December 2023). https://arxiv.org/abs/2311.05762 Cited on The polynomial Freiman-Ruzsa conjecture.
W. T. Gowers, Ben Green, Freddie Manners and Terence Tao, "Marton's Conjecture in abelian groups with bounded torsion", arXiv:2404.02244, 2 April 2024. https://arxiv.org/abs/2404.02244 Cited on The polynomial Freiman-Ruzsa conjecture.
W. T. Gowers, Ben Green, Freddie Manners and Terence Tao, "On a conjecture of Marton", Annals of Mathematics 201 (2025), no. 2, pp. 515–549. doi:10.4007/annals.2025.201.2.5 Cited on The polynomial Freiman-Ruzsa conjecture.
Thomas C. Hales, "A proof of the Kepler conjecture", Annals of Mathematics 162 (3), 2005, pp. 1065–1185. doi:10.4007/annals.2005.162.1065 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Checking instead of convincing.
Thomas Hales and 21 co-authors, "A formal proof of the Kepler conjecture", Forum of Mathematics, Pi 5, e2, 2017. doi:10.1017/fmp.2017.1; preprint arXiv:1501.02155. Cited on What a proof assistant does, Checking instead of convincing.
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux and Maryna Viazovska, "Progress in Formalizing Sphere Packing in Dimension 8", arXiv:2604.23468, April 2026 (revised May 2026). https://arxiv.org/abs/2604.23468 Cited on Research mathematics, Machine learning and theorem proving.
Son Ho and Jonathan Protzenko, "Aeneas: Rust verification by functional translation", Proceedings of the ACM on Programming Languages 6 (ICFP), 2022, pp. 711–741. doi:10.1145/3547647 Cited on Software verification.
W. A. Howard, "The formulae-as-types notion of construction", in J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479–490. Written and circulated in 1969. Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Propositions as types.
Thomas Hubert, Rishi Mehta, Laurent Sartran, et al., "Olympiad-level formal mathematical reasoning with reinforcement learning", Nature 651, pp. 607–613, published online 12 November 2025. doi:10.1038/s41586-025-09833-y Cited on Machine learning and theorem proving.
Gérard P. Huet, "A unification algorithm for typed λ-calculus", Theoretical Computer Science 1(1), 1975, pp. 27–57. doi:10.1016/0304-3975(75)90011-0 Cited on Metavariables and unification.
Antonius J. C. Hurkens, "A simplification of Girard's paradox", in Typed Lambda Calculi and Applications (TLCA 1995), Lecture Notes in Computer Science 902, Springer, 1995, pp. 266–278. https://doi.org/10.1007/BFb0014058 Cited on Universes and Prop, Martin-Löf type theory.^[7]
L. S. van Benthem Jutting, Checking Landau's "Grundlagen" in the Automath System, Mathematical Centre Tracts 83, Mathematisch Centrum, Amsterdam, 1979. ISBN 90-6196-147-5. Record and scan: https://ir.cwi.nl/pub/13104 Cited on Automath.
Jeffrey C. Lagarias, "The 3x+1 problem: an annotated bibliography (1963–1999) (sorted by author)", arXiv:math/0309224 (2003, revised 2011). https://arxiv.org/abs/math/0309224 Cited on Functions that always finish.
Per Martin-Löf, "An intuitionistic theory of types", written 1972 at the University of Stockholm; published in G. Sambin and J. M. Smith (eds.), Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998, pp. 127–172. Copy of the 1972 text: https://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf Cited on Martin-Löf type theory.
Per Martin-Löf, "An intuitionistic theory of types: predicative part", in H. E. Rose and J. C. Shepherdson (eds.), Logic Colloquium '73, Studies in Logic and the Foundations of Mathematics 80, North-Holland, 1975, pp. 73–118. doi:10.1016/S0049-237X(08)71945-1 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Martin-Löf type theory.
Per Martin-Löf, Intuitionistic Type Theory, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Naples, 1984. Re-typeset edition: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf Cited on Martin-Löf type theory.
Per Martin-Löf, "Constructive mathematics and computer programming", in L. J. Cohen, J. Łoś, H. Pfeiffer and K.-P. Podewski (eds.), Logic, Methodology and Philosophy of Science VI, North-Holland, 1982, pp. 153–175. doi:10.1016/S0049-237X(09)70189-2 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Martin-Löf type theory.
Patrick Massot, Floris van Doorn and Oliver Nash, "Formalising the h-principle and sphere eversion", arXiv:2210.07746, October 2022. https://arxiv.org/abs/2210.07746 Cited on Research mathematics.
The mathlib Community, "The Lean mathematical library", in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367–381. doi:10.1145/3372885.3373824; also arXiv:1910.09336. Cited on A library of mathematics, Type classes and instance resolution, Mathlib and its community, Research mathematics, Further reading.
Conor McBride, Healfdene Goguen and James McKinna, "A Few Constructions on Constructors", in Types for Proofs and Programs (TYPES 2004), Lecture Notes in Computer Science 3839, Springer, 2006, pp. 186–200. https://doi.org/10.1007/11617990_12 Cited on Structural and well-founded recursion.
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi and Jean-Baptiste Tristan, "Verified Foundations for Differential Privacy", Proceedings of the ACM on Programming Languages 9 (PLDI), 2025, pp. 1094–1118. doi:10.1145/3729294. arXiv:2412.01671 Cited on Software verification.
Alex Meiburg, Leonardo A. Lessa and Rodolfo R. Soldati, "A Formalization of the Generalized Quantum Stein's Lemma in Lean", arXiv:2510.08672, October 2025. https://arxiv.org/abs/2510.08672 Cited on Physics in Lean.
Dale Miller, "A logic programming language with lambda-abstraction, function variables, and simple unification", Journal of Logic and Computation 1(4), 1991, pp. 497–536. doi:10.1093/logcom/1.4.497 Cited on Metavariables and unification.
Robin Milner, Logic for Computable Functions: Description of a Machine Implementation, Stanford Artificial Intelligence Memo AIM-169, Computer Science Report STAN-CS-72-288, Stanford University, May 1972. http://i.stanford.edu/pub/cstr/reports/cs/tr/72/288/CS-TR-72-288.pdf Cited on LCF and the tactic idea.
Robin Milner, "A theory of type polymorphism in programming", Journal of Computer and System Sciences 17 (3), 1978, pp. 348–375. doi:10.1016/0022-0000(78)90014-4 Cited on LCF and the tactic idea.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, "The Lean Theorem Prover (system description)", in Automated Deduction – CADE-25, Lecture Notes in Computer Science 9195, Springer, 2015, pp. 378–388. doi:10.1007/978-3-319-21401-6_26. Author's copy: https://lean-lang.org/papers/system.pdf Cited on LCF and the tactic idea, Martin-Löf type theory, The Calculus of Constructions, Lean 1 to Lean 3, Further reading.
Leonardo de Moura and Sebastian Ullrich, "The Lean 4 Theorem Prover and Programming Language (System Description)", in Automated Deduction – CADE 28, Lecture Notes in Computer Science 12699, Springer, 2021, pp. 625–635. doi:10.1007/978-3-030-79876-5_37. Author's copy: https://lean-lang.org/papers/lean4.pdf Cited on What a proof assistant does, Why there is no type of all types, Tactics, The small trusted core, Programs and proofs in one language, Inductive types and recursors, Elaboration, The Lean kernel, Type classes and instance resolution, The tactic framework, Decision procedures, Metaprogramming in Lean, The compiler and runtime, LCF and the tactic idea, Lean 1 to Lean 3, Lean 4, Principia Machina, Further reading.^[8]
R. P. Nederpelt, J. H. Geuvers and R. C. de Vrijer (eds.), Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics 133, North-Holland, Amsterdam, 1994. ISBN 0-444-89822-0. Publisher's page with contents: https://shop.elsevier.com/books/selected-papers-on-automath/nederpelt/978-0-444-89822-7 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Automath.
Ulf Norell, Towards a Practical Programming Language Based on Dependent Type Theory, PhD thesis, Chalmers University of Technology and Göteborg University, 2007. https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf Cited on Martin-Löf type theory.
Azim Ospanov, Farzan Farnia and Roozbeh Yousefzadeh, "miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward", arXiv:2511.03108, 5 November 2025. arxiv.org/abs/2511.03108 Cited on Stating the right thing.
Christine Paulin-Mohring, "Inductive definitions in the system Coq: rules and properties", in Typed Lambda Calculi and Applications (TLCA '93), Lecture Notes in Computer Science 664, Springer, 1993, pp. 328–345. doi:10.1007/BFb0037116 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Inductive types and recursors, The Calculus of Constructions.
Christine Paulin-Mohring, "Introduction to the Calculus of Inductive Constructions", in B. Woltzenlogel Paleo and D. Delahaye (eds.), All about Proofs, Proofs for All, Studies in Logic 55, College Publications, 2015. https://inria.hal.science/hal-01094195 Cited on The Calculus of Constructions.
Lawrence C. Paulson, "The foundation of a generic theorem prover", Journal of Automated Reasoning 5 (3), 1989, pp. 363–397. doi:10.1007/BF00248324. Preprint: https://arxiv.org/abs/cs/9301105 Cited on LCF and the tactic idea.
R. Pollack, "How to believe a machine-checked proof", in Giovanni Sambin and Jan M. Smith (eds), Twenty Five Years of Constructive Type Theory, Oxford University Press, 1998, chapter 11 (from p. 205); first issued as BRICS Report RS-97-18, Aarhus University, 1997. doi:10.7146/brics.v4i18.18945 Cited on The small trusted core, What has to be trusted, Checking a proof again later, Stating the right thing, Further reading.
William Pugh, "The Omega test: a fast and practical integer programming algorithm for dependence analysis", Proceedings of the 1991 ACM/IEEE Conference on Supercomputing (Supercomputing '91), ACM, 1991, pp. 4–13. doi:10.1145/125826.125848. Read in an expanded version whose first page states that it appeared in Communications of the ACM in August 1992, there titled "A practical algorithm for exact array dependence analysis", 35(8), pp. 102–114, doi:10.1145/135226.135233. Cited on Decision procedures.
Bertrand Russell, "Mathematical logic as based on the theory of types", American Journal of Mathematics 30 (3), 1908, pp. 222–262. doi:10.2307/2369948 Not read: the pages rest on its bibliographic record or on a secondary account (see Sources). Cited on Why there is no type of all types.
Daniel Selsam, Sebastian Ullrich and Leonardo de Moura, "Tabled Typeclass Resolution", arXiv:2001.04301 [cs.PL], 2020. https://arxiv.org/abs/2001.04301 Cited on Type classes and instance resolution, Further reading.
Joseph Tooby-Smith, "Formalization of physics index notation in Lean 4", arXiv:2411.07667, November 2024. https://arxiv.org/abs/2411.07667 Cited on Physics in Lean.
Joseph Tooby-Smith, "HepLean: Digitalising high energy physics", Computer Physics Communications 308 (2025), article 109457. doi:10.1016/j.cpc.2024.109457; preprint arXiv:2405.08863. Cited on Lean and physics, Physics in Lean.
Joseph Tooby-Smith, "Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature", arXiv:2603.08139, version 2, 20 April 2026. arxiv.org/abs/2603.08139 Cited on Lean and physics.
A. M. Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, series 2, vol. 42 (1936–37), pp. 230–265. doi:10.1112/plms/s2-42.1.230 Cited on Functions that always finish, Automation and its limits.
Sebastian Ullrich and Leonardo de Moura, "Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming", in Proceedings of the 31st Symposium on Implementation and Application of Functional Languages (IFL 2019), ACM, 2019, article 3, pp. 1–12. doi:10.1145/3412932.3412935; preprint arXiv:1908.05647. Cited on The compiler and runtime, Further reading.
Sebastian Ullrich and Leonardo de Moura, "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages", Logical Methods in Computer Science 18(2), 2022, article 1, 21 pp. Extended version of the paper in Automated Reasoning: IJCAR 2020, Lecture Notes in Computer Science 12167, Springer, 2020, pp. 167–182 (doi:10.1007/978-3-030-51054-1_10). doi:10.46298/lmcs-18(2:1)2022; preprint arXiv:2001.10490. Cited on Syntax extension and hygienic macros, Further reading.
Sebastian Ullrich and Leonardo de Moura, "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)", Proceedings of the ACM on Programming Languages 6 (ICFP), article 109, August 2022, 28 pp. doi:10.1145/3547640; author's copy lean-lang.org/papers/do.pdf. Cited on Monads and do-notation.
The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013; Notes to Chapter 1, Example 3.1.9 and §7.2. https://homotopytypetheory.org/book/ Cited on Universes and Prop, Propositional equality.
Philip Wadler, "Propositions as types", Communications of the ACM 58 (12), 2015, pp. 75–84. doi:10.1145/2699407 Cited on What a proof assistant does, Propositions as types, Two kinds of equality.
Benjamin Werner, "Sets in types, types in sets", in Martín Abadi and Takayasu Ito (eds.), Theoretical Aspects of Computer Software (TACS 1997), Lecture Notes in Computer Science 1281, Springer, 1997, pp. 530–546. https://doi.org/10.1007/BFb0014566 Cited on Consistency and the metatheory.
Freek Wiedijk, "A new implementation of Automath", Journal of Automated Reasoning 29 (3–4), 2002, pp. 365–387. doi:10.1023/A:1021983302516. Author's copy: https://www.cs.ru.nl/~freek/aut/aut.pdf Cited on Automath.
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger and Anima Anandkumar, "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models", NeurIPS 2023 Datasets and Benchmarks Track. arXiv:2306.15626 Cited on Machine learning and theorem proving.
Kunhao Zheng, Jesse Michael Han and Stanislas Polu, "MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics", International Conference on Learning Representations (ICLR), 2022. arXiv:2109.00110 Cited on Machine learning and theorem proving.

Lean documentation and source

The Lean Language Reference

The Lean Language Reference, version for Lean 4.34.0, front page and table of contents. lean-lang.org/doc/reference/4.34.0/, consulted 14 October 2026. Cited on Lean theorem prover, Sources, Further reading.
The Lean Language Reference, version 4.34.0, chapter 8 "Axioms": the introduction, §8.2 "Consistency", §8.3 "Reduction", §8.4 "Standard Axioms" and §8.5 "Displaying Axiom Dependencies". https://lean-lang.org/doc/reference/4.34.0/Axioms/ Cited on The three axioms, Sources.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 20.1, "Natural Numbers". https://lean-lang.org/doc/reference/4.34.0/Basic-Types/Natural-Numbers/ Cited on Computation inside proofs, Definitional equality.
"Build Tools and Distribution", a chapter of The Lean Language Reference (edition covering Lean 4.34.0). lean-lang.org/doc/reference/4.34.0/Build-Tools-and-Distribution/ Cited on Lake and Lean projects, Proof export and independent checkers.
The Lean Language Reference, version for Lean 4.34.0, section "Lake". lean-lang.org/doc/reference/4.34.0/Build-Tools-and-Distribution/Lake, consulted 14 October 2026. Cited on A library of mathematics, Lake and Lean projects.
The Lean Language Reference, version for Lean 4.34.0, section "Managing Toolchains with Elan". lean-lang.org/doc/reference/4.34.0/Build-Tools-and-Distribution/Managing-Toolchains-with-Elan, consulted 14 October 2026. Cited on Checking a proof again later, Lake and Lean projects.
Lean Developers, The Lean Language Reference, version 4.34.0, chapter "Coercions". https://lean-lang.org/doc/reference/4.34.0/Coercions/ Cited on Elaboration, Type classes and instance resolution.
The Lean Language Reference, version for Lean 4.34.0, section "Recursive Definitions". lean-lang.org/doc/reference/4.34.0/Definitions/Recursive-Definitions, consulted 14 October 2026. Cited on Functions that always finish, When Lean says no, Programs and proofs in one language, Structural and well-founded recursion.
Lean Developers, The Lean Language Reference, version 4.34.0, chapter "Elaboration and Compilation". https://lean-lang.org/doc/reference/4.34.0/Elaboration-and-Compilation/ Cited on Functions that always finish, Holes and goals, When Lean says no, The small trusted core, Checking a proof again later, Programs and proofs in one language, Terms, types and judgments, Universes and Prop, Structural and well-founded recursion, Definitional equality, Elaboration, The Lean kernel, Metaprogramming in Lean, The compiler and runtime, Glossary.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), "Error Explanations": lean.synthInstanceFailed. https://lean-lang.org/doc/reference/4.34.0/Error-Explanations/About___--synthInstanceFailed/ Cited on When Lean says no.
"Functors, Monads and do-Notation", chapter of The Lean Language Reference (edition covering Lean 4.34.0), introduction and section 18.3 "Syntax". lean-lang.org/doc/reference/4.34.0/Functors___-Monads-and--do--Notation/; …/Syntax/ Cited on Monads and do-notation.
The Lean Language Reference, section 1.1 "History", for version 4.34.0 of Lean. https://lean-lang.org/doc/reference/4.34.0/Introduction/ Cited on Lean 1 to Lean 3, Lean 4, Mathlib and its community, Lean since 2023.
"Custom Operators", section 23.1 of The Lean Language Reference (edition covering Lean 4.34.0). lean-lang.org/doc/reference/4.34.0/Notations-and-Macros/Custom-Operators/ Cited on Syntax extension and hygienic macros.
"Elaborators", section 23.6 of The Lean Language Reference (edition covering Lean 4.34.0). lean-lang.org/doc/reference/4.34.0/Notations-and-Macros/Elaborators/ Cited on Metaprogramming in Lean.
"Macros", section 23.5 of The Lean Language Reference (edition covering Lean 4.34.0), including 23.5.1 "Hygiene", 23.5.3 "Quotation" and 23.5.5 "Defining Macros". lean-lang.org/doc/reference/4.34.0/Notations-and-Macros/Macros/ Cited on Syntax extension and hygienic macros, Metaprogramming in Lean.
"Notations", section 23.3 of The Lean Language Reference (edition covering Lean 4.34.0). lean-lang.org/doc/reference/4.34.0/Notations-and-Macros/Notations/ Cited on Syntax extension and hygienic macros.
"Foreign Function Interface", section 12.4 of The Lean Language Reference (edition covering Lean 4.34.0). lean-lang.org/doc/reference/4.34.0/Run-Time-Code/Foreign-Function-Interface/ Cited on The compiler and runtime.
"Reference Counting", section 12.2 of The Lean Language Reference (edition covering Lean 4.34.0), including 12.2.2 "Compiler IR". lean-lang.org/doc/reference/4.34.0/Run-Time-Code/Reference-Counting/ Cited on The compiler and runtime.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), chapter 14, "Tactic Proofs". https://lean-lang.org/doc/reference/4.34.0/Tactic-Proofs/ Cited on Tactics, Holes and goals, Automation and its limits, The tactic framework.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), section 14.8, "Custom Tactics". https://lean-lang.org/doc/reference/4.34.0/Tactic-Proofs/Custom-Tactics/ Cited on Tactics.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), section 14.5, "Tactic Reference". https://lean-lang.org/doc/reference/4.34.0/Tactic-Proofs/Tactic-Reference/ Cited on Induction, as the machine sees it, Tactics, Holes and goals, Automation and its limits, When Lean says no, Computation inside proofs.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 13.2, "Function Types". https://lean-lang.org/doc/reference/4.34.0/Terms/Function-Types/ Cited on Dependent function types.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 13.3, "Functions". https://lean-lang.org/doc/reference/4.34.0/Terms/Functions/ Cited on Notation.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), chapter 16, "The grind tactic". https://lean-lang.org/doc/reference/4.34.0/The--grind--tactic/ Cited on Automation and its limits, Decision procedures, Lean since 2023.
The Lean Language Reference, version for Lean 4.34.0 (lean-lang.org, 2026), chapter 15, "The Simplifier". https://lean-lang.org/doc/reference/4.34.0/The-Simplifier/ Cited on Automation and its limits, Decision procedures.
The Lean Language Reference, version for Lean 4.34.0, chapter 4, "The Type System". lean-lang.org/doc/reference/4.34.0/The-Type-System/, consulted 14 October 2026. Cited on Terms, types and judgments, Definitional equality, Proof irrelevance and subsingleton elimination, Glossary.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 4.1, "Functions". https://lean-lang.org/doc/reference/4.34.0/The-Type-System/Functions/ Cited on Dependent function types, Structural and well-founded recursion, Definitional equality, Notation.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 4.4, "Inductive Types". https://lean-lang.org/doc/reference/4.34.0/The-Type-System/Inductive-Types/ Cited on Building things from constructors, Induction, as the machine sees it, Universes and Prop, Inductive types and recursors, Structural and well-founded recursion, Propositional equality, Proof irrelevance and subsingleton elimination.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, section 4.2, "Propositions". https://lean-lang.org/doc/reference/4.34.0/The-Type-System/Propositions/ Cited on Universes and Prop, The three axioms, Proof irrelevance and subsingleton elimination.
The Lean Language Reference, version 4.34.0, §4.5 "Quotients": the introduction, §4.5.5 "Logical Model", §4.5.5.2 "Quotients and Inductive Types", §4.5.6 "Quotients and Function Extensionality" and §4.5.7 "Squash Types". https://lean-lang.org/doc/reference/4.34.0/The-Type-System/Quotients/ Cited on Propositional equality, Quotient types.
The Lean Language Reference, version for Lean 4.34.0, section 4.3, "Universes". lean-lang.org/doc/reference/4.34.0/The-Type-System/Universes/, consulted 14 October 2026. Cited on Universes and Prop, Glossary.
Lean Developers, The Lean Language Reference, version 4.34.0, chapter "Type Classes", and its section "Instance Synthesis". https://lean-lang.org/doc/reference/4.34.0/Type-Classes/ Cited on Type classes and instance resolution.
The Lean Language Reference, version for Lean 4.34.0, section "Validating a Lean Proof". lean-lang.org/doc/reference/4.34.0/ValidatingProofs, consulted 14 October 2026. Cited on Tactics, Holes and goals, Computation inside proofs, What has to be trusted, Checking a proof again later, Stating the right thing, The three axioms, Consistency and the metatheory, Elaboration, The Lean kernel, Decision procedures, Syntax extension and hygienic macros, Metaprogramming in Lean, The compiler and runtime, Lake and Lean projects, Proof export and independent checkers, Lean since 2023.
"Lean 4.22.0", in "Release Notes", The Lean Language Reference (edition covering Lean 4.34.0), Highlights, "New compiler". lean-lang.org/doc/reference/4.34.0/releases/v4.22.0/ Cited on The compiler and runtime.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, release notes, "Lean 4.27.0", section "Language". https://lean-lang.org/doc/reference/4.34.0/releases/v4.27.0/ Cited on Structural and well-founded recursion.
"Lean 4.28.0", in "Release Notes", The Lean Language Reference (edition covering Lean 4.34.0), section "External Checker". lean-lang.org/doc/reference/4.34.0/releases/v4.28.0/ Cited on Proof export and independent checkers.
"Lean 4.32.0", in "Release Notes", The Lean Language Reference (edition covering Lean 4.34.0), Highlights and Language sections. lean-lang.org/doc/reference/4.34.0/releases/v4.32.0/ Cited on Monads and do-notation.
The Lean Language Reference, version for Lean 4.34.0, "Lean 4.32.1 (2026-07-22)", release notes. lean-lang.org/doc/reference/4.34.0/releases/v4.32.1, consulted 14 October 2026. Cited on What has to be trusted, Lean since 2023.
The Lean Language Reference, version for Lean 4.34.0, "Lean 4.32.2 (2026-07-28)", release notes. lean-lang.org/doc/reference/4.34.0/releases/v4.32.2, consulted 14 October 2026. Cited on What has to be trusted, Lean since 2023.
The Lean Language Reference, for Lean 4.34.0, lean-lang.org, 2026, release notes, "Lean 4.8.0" (functional induction principles) and "Lean 4.18.0" (the fun_induction tactic). https://lean-lang.org/doc/reference/4.34.0/releases/v4.8.0/ and https://lean-lang.org/doc/reference/4.34.0/releases/v4.18.0/ Cited on Structural and well-founded recursion.
The Lean Language Reference, version for Lean 4.35.0, front page and table of contents. lean-lang.org/doc/reference/4.35.0/, consulted 14 October 2026. Cited on Sources.
The Lean Developers, "Axioms", The Lean Language Reference, for Lean 4.35.0, chapter 8. lean-lang.org/doc/reference/4.35.0/Axioms/ (accessed 13 October 2026). Cited on Why there is no type of all types, What the axioms are, Sources.
The Lean Developers, "Finite natural numbers", The Lean Language Reference, for Lean 4.35.0, section 21.3. lean-lang.org/doc/reference/4.35.0/Basic-Types/Finite-Natural-Numbers/ (accessed 14 October 2026). Cited on Types as specifications.
The Lean Developers, "Subtypes", The Lean Language Reference, for Lean 4.35.0, section 21.20. lean-lang.org/doc/reference/4.35.0/Basic-Types/Subtypes/ (accessed 14 October 2026). Cited on Types as specifications.
The Lean Developers, "Introduction", The Lean Language Reference, for Lean 4.35.0, section 1.1, "History". lean-lang.org/doc/reference/4.35.0/Introduction/ (accessed 14 October 2026). Cited on What a proof assistant does, Checking instead of convincing.
The Lean Developers, "The type system", The Lean Language Reference, for Lean 4.35.0, chapter 4. lean-lang.org/doc/reference/4.35.0/The-Type-System/ (accessed 13 October 2026). Cited on Checking instead of convincing, Types as specifications, Two kinds of equality.
The Lean Developers, "Propositions", The Lean Language Reference, for Lean 4.35.0, section 4.2. lean-lang.org/doc/reference/4.35.0/The-Type-System/Propositions/ (accessed 13 October 2026). Cited on Why there is no type of all types, What the axioms are.
The Lean Developers, "Universes", The Lean Language Reference, for Lean 4.35.0, section 4.3. lean-lang.org/doc/reference/4.35.0/The-Type-System/Universes/ (accessed 13 October 2026). Cited on Why there is no type of all types.
The Lean Developers, "Validating a Lean proof", The Lean Language Reference, for Lean 4.35.0. lean-lang.org/doc/reference/4.35.0/ValidatingProofs/ (accessed 13 October 2026). Cited on What a proof assistant does, What the axioms are, Sources.
The Lean Language Reference, version for Lean 4.35.0, "Release Notes", list of versions with their dates. lean-lang.org/doc/reference/4.35.0/releases/, consulted 14 October 2026. Cited on Sources.
The Lean Language Reference, "Release Notes", list of versions with their dates (read 14 October 2026). https://lean-lang.org/doc/reference/latest/releases/ Cited on Lean since 2023, Chronology.
The Lean Language Reference, "Lean 4.22.0 (2025-08-14)", release notes. https://lean-lang.org/doc/reference/latest/releases/v4.22.0/ Cited on Lean since 2023.^[9]

Source code

Batteries (README). github.com/leanprover-community/batteries, consulted 14 October 2026. Cited on A library of mathematics.
Lean 3 community edition, README file and its earlier version. https://github.com/leanprover-community/lean Cited on Lean 1 to Lean 3.
Lean 3 community edition, change log (doc/changes.md), entries from v3.2.0 (June 2017) to 3.51.1c (24 May 2023). https://github.com/leanprover-community/lean/blob/master/doc/changes.md Cited on Lean 1 to Lean 3.
Lean 3 mathlib, README file. https://github.com/leanprover-community/mathlib Cited on Lean 4, Mathlib and its community.
Mathlib, README of the Lean 4 library. https://github.com/leanprover-community/mathlib4 Cited on Mathlib and its community.
Mathlib, source file Mathlib/Basic/Real/Basic.lean, module documentation "Real numbers from Cauchy sequences". github.com/leanprover-community/mathlib4, consulted 14 October 2026. Cited on Lean and physics.
Mathport, README file. https://github.com/leanprover-community/mathport Cited on Lean 4.
Lean 2 source code, README file ("This is a snapshot of the Lean 0.2 theorem prover..."). https://github.com/leanprover/lean2 Cited on Lean 1 to Lean 3.
Lean 3 source code, README file, notice that the code is frozen and Lean 4 is the official line. https://github.com/leanprover/lean3 Cited on Lean 1 to Lean 3.
Lean 3 source code, version tag v3.0.0, published 20 January 2017. https://github.com/leanprover/lean3/releases/tag/v3.0.0 Cited on Lean 1 to Lean 3.
Lean 4 source, file src/Init/Classical.lean, version 4.34.1: Classical.em ("Diaconescu's theorem"), Classical.choose and Classical.propDecidable. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Init/Classical.lean Cited on Classical logic from choice.
Lean 4 source, file src/Init/Core.lean, version 4.34.1: the definitions of Setoid, Quotient and Quotient.exact. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Init/Core.lean Cited on Quotient types, The compiler and runtime.
Lean 4 source code, version 4.34.1 (2026), file src/Init/Grind/Tactics.lean: the documentation string of the grind tactic. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Init/Grind/Tactics.lean Cited on Decision procedures.
Lean 4 source, file src/Init/Prelude.lean, version 4.34.1: the init_quot command and the documentation of Quot, Quot.mk, Quot.lift, Quot.ind, Quot.sound and Quot.lcInv. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Init/Prelude.lean Cited on Propositional equality, Quotient types, Elaboration.
Lean 4 source code, version 4.34.1 (2026), file src/Init/Tactics.lean: the documentation strings and definitions of all_goals, focus, first, try, <;>, repeat, exact? and apply?. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Init/Tactics.lean Cited on The tactic framework, Decision procedures.
Lean 4 source code, version 4.34.1 (2026), files src/Lean/Elab/Notation.lean (the functions elabNotation and mkUnexpander) and src/Lean/Elab/Macro.lean (the function elabMacro). Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/Notation.lean Cited on Syntax extension and hygienic macros.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Elab/SyntheticMVars.lean: the function synthesizeSyntheticMVars. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/SyntheticMVars.lean Cited on Elaboration, The tactic framework.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Elab/Tactic/BVDecide.lean: the overview of bv_decide, sections "Architecture" and "Axioms". Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/Tactic/BVDecide.lean Cited on Decision procedures.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Elab/Tactic/Basic.lean: the definitions TacticM, Tactic, getGoals and tryCatchRestore, with the structure Tactic.State in src/Lean/Elab/Term/TermElabM.lean. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/Tactic/Basic.lean Cited on The tactic framework.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Elab/Tactic/Omega.lean: implementation notes of the omega tactic. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/Tactic/Omega.lean Cited on Decision procedures.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Elab/Term/TermElabM.lean: the function elabTermAux and the type SyntheticMVarKind. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Elab/Term/TermElabM.lean Cited on Elaboration, The tactic framework.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Environment.lean: the structure Lean.Kernel.Environment, the option debug.skipKernelTC and the function addDeclWithoutChecking. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Environment.lean Cited on The Lean kernel.
Lean 4 source, src/Lean/Expr.lean, documentation of Expr.bvar, version 4.34.1. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Expr.lean Cited on Automath.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Message.lean: the messages for Kernel.Exception. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Message.lean Cited on The Lean kernel.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Meta/ExprDefEq.lean: the notes on pattern unification and its approximations A1 to A7. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Meta/ExprDefEq.lean Cited on Metavariables and unification.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/Meta/SynthInstance.lean: the notes on tabled resolution and table keys, the function generate, and the notes on outParam. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Meta/SynthInstance.lean Cited on Type classes and instance resolution.
Lean 4 source code, version 4.34.1 (2026), file src/Lean/MetavarContext.lean: the design notes at the head of the file. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/MetavarContext.lean Cited on Metavariables and unification, The tactic framework.
Lean 4 source, file src/Lean/Parser/Term.lean, version 4.34.1: the documentation comment of the h ▸ e syntax. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Parser/Term.lean Cited on Propositional equality.
Lean 4 source code, version 4.34.1 (2026), file src/Std/Tactic/BVDecide/Reflect.lean: the definition verifyBVExpr and the theorem unsat_of_verifyBVExpr_eq_true. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/Std/Tactic/BVDecide/Reflect.lean Cited on Decision procedures.
Lean 4 source code, version 4.34.1 (2026), file src/kernel/environment.cpp: the functions add_axiom, add_definition, add_theorem, add_opaque, add_mutual and check_constant_val. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/kernel/environment.cpp Cited on The Lean kernel.
Lean 4 source code, version 4.34.1 (2026), file src/kernel/inductive.cpp: the functions check_constructors and check_positivity. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/kernel/inductive.cpp Cited on The Lean kernel.
Lean 4 source code, version 4.34.1 (2026), file src/kernel/type_checker.cpp: the functions is_def_eq_core, lazy_delta_reduction_step and reduce_nat; with the function compare in src/kernel/declaration.cpp, which orders unfolding by definitional height. Apache License 2.0. https://github.com/leanprover/lean4/blob/v4.34.1/src/kernel/type_checker.cpp Cited on The Lean kernel.
Lean 4 source code, version tag v4.0.0, published 8 September 2023. https://github.com/leanprover/lean4/releases/tag/v4.0.0 Cited on Lean 4.
Lean 4 source, version 4.34.1: files src/Init/Core.lean (propext), src/Init/Prelude.lean (Quot.sound, Classical.choice, sorryAx) and src/Init/Classical.lean (the proof of Classical.em). Apache License 2.0. https://github.com/leanprover/lean4/tree/v4.34.1/src/Init Cited on The three axioms.
Lean 4 source code, version 4.34.1 (2026), directory src/Lean/Compiler/LCNF: in Passes.lean the passes of the impure phase (insertResetReuse, inferBorrow, explicitBoxing, explicitRc, expandResetReuse), in Main.lean the translation of their result to IR (IR.toIR), and EmitC.lean, which emits C. Apache License 2.0. https://github.com/leanprover/lean4/tree/v4.34.1/src/Lean/Compiler/LCNF Cited on The compiler and runtime.
Lean 4 source code, version 4.34.1 (2026), directory src/kernel (36 files *.cpp and *.h, plus CMakeLists.txt). Apache License 2.0. https://github.com/leanprover/lean4/tree/v4.34.1/src/kernel Cited on The Lean kernel.
lean4checker (README of the archived project; now distributed with Lean as leanchecker). github.com/leanprover/lean4checker, consulted 13 October 2026. Cited on Checking a proof again later.
lean4export (README). github.com/leanprover/lean4export, consulted 13 October 2026. Cited on Checking a proof again later.
"lean4export", Reservoir, the index of Lake packages: "A simple declaration exporter for Lean 4 using the Lean 4 NDJSON export format". reservoir.lean-lang.org/@leanprover/lean4export Cited on Proof export and independent checkers.

Projects and announcements

ACM SIGPLAN, "Programming Languages Software Award", recipients, 2025: Lean Theorem Prover. https://www.sigplan.org/Awards/Software/ Cited on Lean since 2023.
Adam Topaz, "Definitions in the liquid tensor experiment", Lean community blog, 14 October 2022. https://leanprover-community.github.io/blog/posts/lte-examples/ Cited on The Liquid Tensor Experiment.
Alexander Bentkamp, Jon Eugster et al., "Lean 4 Game", the source of the Lean Game Server: project description and list of hosted games, read 14 October 2026. https://github.com/leanprover-community/lean4game Cited on Teaching with Lean.
Announcement of the 1991 ACM Turing Award to Robin Milner, with the short citation, forwarded to the TYPES mailing list, 1 November 1991. https://www.engineering.upenn.edu/~sweirich/types/archive/1991/msg00062.html Cited on LCF and the tactic idea.
Anthropic, "Formalizing Fermat's Last Theorem", 4 September 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem Cited on The Fermat's Last Theorem project, Machine learning and theorem proving.
CADE Inc., "Skolem Award", with the list of recipients (awards at CADE-30, July 2025). https://cadeinc.org/Skolem-Award Cited on Lean since 2023.
EPFL, "Prof. Viazovska's proofs of sphere packing formalized with AI", EPFL news, March 2026. https://actu.epfl.ch/news/prof-viazovska-s-proofs-of-sphere-packing-formaliz/ Cited on Research mathematics.
Floris van Doorn et al., "Formalization of a generalized Carleson's theorem" (project description, read 13 October 2026). https://github.com/fpvandoorn/carleson Cited on Research mathematics.
Freek Wiedijk, "Automath" (notes accompanying the aut checker). https://www.cs.ru.nl/~freek/aut/ Cited on Automath.
Google DeepMind, "AI achieves silver-medal standard solving International Mathematical Olympiad problems", 25 July 2024. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ Cited on Lean since 2023, Machine learning and theorem proving.
Isabelle, home page. isabelle.in.tum.de (accessed 13 October 2026). Cited on What a proof assistant does.
Johan Commelin, "Liquid Tensor Experiment: an update", Lean community blog, 31 December 2021. https://leanprover-community.github.io/blog/posts/lte-update/ Cited on The Liquid Tensor Experiment.
John Harrison, The HOL Light theorem prover, home page. www.cl.cam.ac.uk/~jrh13/hol-light/ (accessed 14 October 2026). Cited on What a proof assistant does.
Kesha Hietala and Emina Torlak, "Lean Into Verified Software Development", AWS Open Source Blog, 8 April 2024. https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/ Cited on Software verification.
Kevin Buzzard, "A Lean formalisation of Fermat's Last Theorem" (the project's general information), written December 2023. https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md Cited on Research mathematics, The Fermat's Last Theorem project, Teaching with Lean.
Kevin Buzzard, "AI at IMO 2025: a round-up", Xena (blog), 3 August 2025. https://xenaproject.wordpress.com/2025/08/03/ai-at-imo-2025-a-round-up/ Cited on Machine learning and theorem proving.
Kevin Buzzard et al., "Fermat's Last Theorem" (project page and README), Imperial College London, read 14 October 2026. https://imperialcollegelondon.github.io/FLT/ and https://github.com/ImperialCollegeLondon/FLT Cited on The Fermat's Last Theorem project.
Kevin Buzzard, "Fermat's Last Theorem — how it's going", Xena (blog), 11 December 2024. https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ Cited on Research mathematics, The Fermat's Last Theorem project.
Kevin Buzzard, "FLT: Anthropic has beaten me to it", Xena (blog), 4 September 2026. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ Cited on Research mathematics, The Fermat's Last Theorem project, Machine learning and theorem proving.
Kevin Buzzard, "Formalizing Fermat workshop", Xena (blog), 15 May 2026. https://xenaproject.wordpress.com/2026/05/15/formalizing-fermat-workshop/ Cited on The Fermat's Last Theorem project, Machine learning and theorem proving.
Kevin Buzzard, Jon Eugster et al., Natural Number Game, Lean 4 version, game text and credits. https://github.com/leanprover-community/NNG4 Cited on Teaching with Lean.
Kevin Buzzard, Jon Eugster et al., Natural Number Game, Lean 4 version, on the Lean Game Server: https://adam.math.hhu.de/#/g/leanprover-community/nng4 (source and credits: https://github.com/leanprover-community/NNG4) Cited on Further reading.
Kevin Buzzard, "The Annals Challenge", Xena (blog), 13 August 2026. https://xenaproject.wordpress.com/2026/08/13/the-annals-challenge/ Cited on Research mathematics, Machine learning and theorem proving.
Kevin Buzzard, "The Fermat's Last Theorem Project", Lean community blog, 30 April 2024. https://leanprover-community.github.io/blog/posts/FLT-announcement/ Cited on The Fermat's Last Theorem project.
Lean community, "Community teams" and "Mathlib reviewers" (read 14 October 2026). https://leanprover-community.github.io/teams.html Cited on Mathlib and its community.
Lean community, "Contributing to mathlib" (read 14 October 2026). https://leanprover-community.github.io/contribute/index.html Cited on Mathlib and its community.
Lean community, "Mathlib maintainers" (read 14 October 2026). https://leanprover-community.github.io/teams/maintainers.html Cited on Mathlib and its community.
Lean community, "Mathlib porting status" (read 14 October 2026). https://leanprover-community.github.io/mathlib-port-status/ Cited on Lean 4.
Lean community, "Mathlib statistics". leanprover-community.github.io/mathlib_stats.html, consulted 14 October 2026. Cited on A library of mathematics, Mathlib and its community.
Lean FRO, "About" page, with its timeline "A Brief History of Lean" (read 14 October 2026). https://lean-lang.org/fro/about/ Cited on Lean since 2023.
Lean FRO, home page, "Vision" and "Mission" (read 14 October 2026). https://lean-lang.org/fro/ Cited on Lean since 2023.
Lean FRO, "Roadmap" (index of the roadmaps from August 2023). https://lean-lang.org/fro/roadmap/ Cited on Lean since 2023.
Lean FRO, "The Lean FRO Year 4 - Part 1 Roadmap", covering September 2026 to February 2027. https://lean-lang.org/fro/roadmap/y4-1/ Cited on Lean since 2023.
Lean Kernel Arena. arena.lean-lang.org, consulted 13 October 2026. Cited on Checking a proof again later, Proof export and independent checkers.
"lean4lean", checker page, Lean Kernel Arena. arena.lean-lang.org/checker/lean4lean Cited on Proof export and independent checkers.
Leonardo de Moura, "Postmortem for Kernel Soundness Bug #14576", 1 August 2026. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ Cited on Lean since 2023.
"nanoda", checker page, Lean Kernel Arena. arena.lean-lang.org/checker/nanoda/ Cited on Proof export and independent checkers.
nanoda_lib (README), an external type checker for Lean 4 written in Rust. github.com/ammkrn/nanoda_lib, consulted 13 October 2026. Cited on Checking a proof again later.
Peter Scholze, "Half a year of the Liquid Tensor Experiment: amazing developments", guest post on the Xena blog, 5 June 2021. xenaproject.wordpress.com (accessed 13 October 2026). Cited on Checking instead of convincing, The Liquid Tensor Experiment, Research mathematics.
Peter Scholze, "Liquid tensor experiment", guest post on the Xena blog, 5 December 2020. xenaproject.wordpress.com (accessed 13 October 2026). Cited on Checking instead of convincing, The Liquid Tensor Experiment.
Physlib, "About Physlib", project website, read 14 October 2026. https://physlib.io/about Cited on Physics in Lean.
Physlib (README). github.com/leanprover-community/physlib, consulted 14 October 2026; also physlib.io. Cited on Lean and physics, Physics in Lean.
"Principia Machina: the move to Lean", the page Principia Machina/Lean transition on this wiki, status as of 14 October 2026. Cited on Physics in Lean, Principia Machina.
Renaissance Philanthropy, "Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics: A Mathlib Initiative Interview", 3 October 2025. https://www.renaissancephilanthropy.org/insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview Cited on Mathlib and its community.
Renaissance Philanthropy, "Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research", 24 July 2025. https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research Cited on Mathlib and its community, Lean since 2023.
Son Ho, Cédric Fournet, Antoine Delignat-Lavaud, Samuel Lee, Jason Fisher and Jessica Krynitsky, "Verifying Rust cryptography in SymCrypt, from standards to code", Microsoft Research Blog, 13 July 2026. https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/ Cited on Software verification, Machine learning and theorem proving.
Terence Tao, "A pilot project in universal algebra to explore new ways to collaborate and use machine assistance?", What's new (blog), 25 September 2024. https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/ Cited on The equational theories project.
Terence Tao, "Formalizing the proof of PFR in Lean4 using Blueprint: a short tour", What's new (blog), 18 November 2023. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ Cited on The polynomial Freiman-Ruzsa conjecture.
Terence Tao, "On a conjecture of Marton", What's new (blog), 13 November 2023. https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/ Cited on The polynomial Freiman-Ruzsa conjecture.
Terence Tao, post on Mathstodon, 5 December 2023. https://mathstodon.xyz/@tao/111526765350663641 Cited on The polynomial Freiman-Ruzsa conjecture.
Terence Tao, Yaël Dillies et al., "The Polynomial Freiman-Ruzsa Conjecture" (project page, with blueprint and Lean source), read 14 October 2026. https://teorth.github.io/pfr/ Cited on The polynomial Freiman-Ruzsa conjecture.
The Agda Team, "What is Agda?", Agda documentation. agda.readthedocs.io (accessed 13 October 2026). Cited on What a proof assistant does.
The Automath Archive, Eindhoven University of Technology, "About Automath". https://automath.win.tue.nl/aboutautomath.htm Cited on Automath.
"The collected works of Per Martin-Löf", an online archive of his papers, list of works with dates. https://archive-pml.github.io/ Cited on Martin-Löf type theory.
"The first official release of Lean 4", Lean community blog, 8 September 2023. https://leanprover-community.github.io/blog/posts/first-lean-release/ Cited on Lean 4, Lean since 2023.
The mathlib community, "Completion of the Liquid Tensor Experiment", Lean community blog, 15 July 2022. https://leanprover-community.github.io/blog/posts/lte-final/ Cited on The Liquid Tensor Experiment, Research mathematics.
The Rocq Prover Reference Manual, "History of Coq", including "A short history of the early versions" written by Thierry Coquand, Gérard Huet and Christine Paulin-Mohring in September 2015 and Huet's summary of February 1995. https://rocq-prover.org/doc/master/refman/history.html Cited on The Calculus of Constructions.
The Rocq Team, "About Rocq", The Rocq Prover. rocq-prover.org/about (accessed 13 October 2026). Cited on What a proof assistant does, The Calculus of Constructions.
The Rocq Team, "Rocq 9.0.0", The Rocq Prover, 12 March 2025. rocq-prover.org/releases/9.0.0 (accessed 13 October 2026). Cited on What a proof assistant does, The Calculus of Constructions.
The Xena Project (blog), "Division by zero in type theory: a FAQ", 5 July 2020. xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq Cited on Stating the right thing.
"Tutorial" test suite, Lean Kernel Arena. arena.lean-lang.org/tutorial/ Cited on Proof export and independent checkers.
UK Research and Innovation, Gateway to Research, "Formalising Fermat", grant EP/Y022904/1, principal investigator Kevin Buzzard, Imperial College London. https://gtr.ukri.org/projects?ref=EP%2FY022904%2F1 Cited on The Fermat's Last Theorem project.
University of Bonn, Department of Mathematics, "Skolem Award for Floris van Doorn", 27 May 2025. https://www.mathematics.uni-bonn.de/en/news/skolem-award-for-floris-van-doorn Cited on Lean since 2023.
"Update on mathport (Dec 2021)", Lean community blog, 22 December 2021. https://leanprover-community.github.io/blog/posts/intro-to-mathport/ Cited on Lean 4.

Press and encyclopedias

B. Jack Copeland, "The Church-Turing Thesis", The Stanford Encyclopedia of Philosophy (first published 1997, substantive revision 18 December 2023), section 1.7. https://plato.stanford.edu/entries/church-turing/ Cited on Automation and its limits.
Bernard Linsky and Andrew David Irvine, "Principia Mathematica", The Stanford Encyclopedia of Philosophy, substantive revision of 10 March 2026. plato.stanford.edu/entries/principia-mathematica/ (accessed 13 October 2026). Cited on Why there is no type of all types.
Davide Castelvecchi, "Mathematicians welcome computer-assisted proof in 'grand unification' theory", Nature 595, 2021, pp. 18–19 (news, 18 June 2021). doi:10.1038/d41586-021-01627-2 Read in part: the headline, the summary and the first paragraph; the rest is behind a paywall (see Sources). Cited on The Liquid Tensor Experiment.
Harry Deutsch, Oliver Marshall and Andrew David Irvine, "Russell's paradox", The Stanford Encyclopedia of Philosophy, substantive revision of 13 March 2026. plato.stanford.edu/entries/russell-paradox/ (accessed 13 October 2026). Cited on Why there is no type of all types.
John L. Bell, "The Axiom of Choice", Stanford Encyclopedia of Philosophy, substantive revision of 10 December 2021, §5 "The Axiom of Choice and Logic" and note 15. https://plato.stanford.edu/entries/axiom-choice/ Cited on Classical logic from choice.
Kevin Hartnett, "Proof Assistant Makes Jump to Big-League Math", Quanta Magazine, 28 July 2021. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ Cited on The Liquid Tensor Experiment.
Leila Sloman, "'A-Team' of Math Proves a Critical Link Between Addition and Sets", Quanta Magazine, 6 December 2023. https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ Cited on The polynomial Freiman-Ruzsa conjecture.
Liesbeth De Mol, "Turing Machines", The Stanford Encyclopedia of Philosophy (first published 2018, substantive revision 21 May 2025), section 2.4. https://plato.stanford.edu/entries/turing-machine/ Cited on Functions that always finish.
Mathematics Genealogy Project, entry for Lambert S. van Benthem Jutting: Ph.D., Technische Universiteit Eindhoven, 1977, dissertation "Checking Landau's 'Grundlagen' in the Automath System", advisors N. G. de Bruijn and W. Peremans. https://www.mathgenealogy.org/id.php?id=63580 Cited on Automath.
nLab, "Burali-Forti's paradox", section "In type theory: Girard's paradox", revision of 24 November 2023. https://ncatlab.org/nlab/show/Girard%27s+paradox Cited on Universes and Prop.
Panu Raatikainen, "Gödel's Incompleteness Theorems", The Stanford Encyclopedia of Philosophy (first published 2013, substantive revision 8 October 2025), sections 1 and 4.2. https://plato.stanford.edu/entries/goedel-incompleteness/ Cited on Automation and its limits, Consistency and the metatheory.
Peter Dybjer and Erik Palmgren, "Intuitionistic type theory", The Stanford Encyclopedia of Philosophy, substantive revision of 23 September 2024, sections 3.6 and 7.4. plato.stanford.edu/entries/type-theory-intuitionistic/ (accessed 13 October 2026). Cited on Why there is no type of all types, Martin-Löf type theory.
Thierry Coquand, "Type theory", The Stanford Encyclopedia of Philosophy, substantive revision of 6 September 2022, section 6. plato.stanford.edu/entries/type-theory/ (accessed 13 October 2026). Cited on Why there is no type of all types.

References

↑ Terms, types and judgments gives the journal as Indagationes Mathematicae (Proceedings) 75 (5); Automath gives both numberings, as above.
↑ The Calculus of Constructions cites the PDF attached to the release, as a thesis of April 2019; the other pages cite the release page.
↑ Checking a proof again later, What has to be trusted and Consistency and the metatheory cite version 3 of the arXiv text, of 14 September 2025. The paper's TYPES 2025 version is listed separately; Definitional equality, Inductive types and recursors and Terms, types and judgments cite that version and say they read version 2 of the arXiv text.
↑ Definitional equality, Inductive types and recursors and Terms, types and judgments say they read the text in arXiv version 2; Two kinds of equality calls the arXiv text a preprint, Proof export and independent checkers its full version. Version 3 of the arXiv text is listed separately.
↑ Read for Universes and Prop; The Calculus of Constructions cites it from its bibliographic record.
↑ LCF and the tactic idea and Martin-Löf type theory cite the author's PDF copy, www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf, under the name Mike Gordon; Automation and its limits and Tactics cite the HTML copy given here.
↑ Read for Universes and Prop; Martin-Löf type theory cites it from its bibliographic record.
↑ Principia Machina, Tactics, What a proof assistant does and Why there is no type of all types give the title without "(System Description)"; Inductive types and recursors, Programs and proofs in one language and The small trusted core omit the volume number 12699.
↑ The same notes, in the edition of the manual for Lean 4.34.0, are listed above, cited on The compiler and runtime. This citation uses the address under "latest", which follows the newest version.
↑ LCF and the tactic idea cites the chapter at its earlier address, lean-lang.org/theorem_proving_in_lean4/tactics.html, which now forwards here.

[1] Terms, types and judgments gives the journal as Indagationes Mathematicae (Proceedings) 75 (5); Automath gives both numberings, as above.

[2] The Calculus of Constructions cites the PDF attached to the release, as a thesis of April 2019; the other pages cite the release page.

[3] Checking a proof again later, What has to be trusted and Consistency and the metatheory cite version 3 of the arXiv text, of 14 September 2025. The paper's TYPES 2025 version is listed separately; Definitional equality, Inductive types and recursors and Terms, types and judgments cite that version and say they read version 2 of the arXiv text.

[4] Definitional equality, Inductive types and recursors and Terms, types and judgments say they read the text in arXiv version 2; Two kinds of equality calls the arXiv text a preprint, Proof export and independent checkers its full version. Version 3 of the arXiv text is listed separately.

[5] Read for Universes and Prop; The Calculus of Constructions cites it from its bibliographic record.

[6] LCF and the tactic idea and Martin-Löf type theory cite the author's PDF copy, www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf, under the name Mike Gordon; Automation and its limits and Tactics cite the HTML copy given here.

[7] Read for Universes and Prop; Martin-Löf type theory cites it from its bibliographic record.

[8] Principia Machina, Tactics, What a proof assistant does and Why there is no type of all types give the title without "(System Description)"; Inductive types and recursors, Programs and proofs in one language and The small trusted core omit the volume number 12699.

[9] The same notes, in the edition of the manual for Lean 4.34.0, are listed above, cited on The compiler and runtime. This citation uses the address under "latest", which follows the newest version.

[10] LCF and the tactic idea cites the chapter at its earlier address, lean-lang.org/theorem_proving_in_lean4/tactics.html, which now forwards here.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]