Elamur Research
☰
home / papers / 2021 / The Lean 4 Theorem Prover and Programming Language (System Description)

The Lean 4 Theorem Prover and Programming Language (System Description)

Written for the Research library (claude-opus-5-5) from the paper text. Original — link.springer.com/content/pdf/10.1007/978-3-030-79876-5 37.pdf

Summary

Lean 3 owed much of its success to metaprogramming. However, large parts of the system were written in C++ and could not be changed by users. Its metaprograms also ran on an interpreting virtual machine, so custom proof automation lagged behind tools written in OCaml or C++. Lean 4 solves this by rewriting the prover in Lean itself. By importing the Lean package, users gain access to every internal data structure and can customize the system's core components, from the code generator and pretty printer to the decision procedures, tactics, elaborator and parser. The paper introduces the language through a BoolExpr example: a small simplifier, an evaluator, and a correctness proof using induction and simp. It then describes the main new components: tabled typeclass resolution, a capture-avoiding macro system designed for ITPs, a compiler that emits C, reference-counted memory with in-place reuse, and an incremental LSP server. Early measurements suggest the generated code competes with, and often beats, ocamlopt and GHC. This matters because mathlib and similar projects rely on fast automation written by users.

Key points

  • Lean 4 was released as open source in early 2021. The community is porting mathlib, which started in 2017 under Lean 3 and has about half a million lines. Early adopters built a Reopt translation verifier, an inductive-inductive types package and a car controller.
  • Typeclass resolution now uses tabling (generalized memoization) plus discrimination trees for indexing. This removes the exponential slowdowns Lean 3 suffered with instance diamonds.
  • The hygienic macro system draws on Scheme. It prevents accidental name capture in tactics, and Lean 3's notation command is reimplemented as a macro that generates macros.
  • The compiler applies GHC-inspired transformations controlled by @[inline]/@[specialize]. It erases proofs and lowers code to an IR (Lean.Compiler.IR) that can target other backends. An IR interpreter switches to precompiled native code whenever it is available.
  • The "functional but in-place" (FBIP) paradigm rests on a "resurrection hypothesis": objects often die just before a new object of the same kind is created. Reference counting lets the runtime reuse such unshared objects, so map over an unshared list allocates nothing. Arrays and hashtables can be used in pure code at no cost when they are unshared.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Fields: Mathematics & statistics

Cited by

150 papers of our library cite it (of the 140673 whose bibliographies we read); 4 of them have a page here, 146 not yet.

Cite

The paper itself, not this page. BibTeX from the library's record of the work.

@article{moura2021lean,
  title = {{The Lean 4 Theorem Prover and Programming Language (System Description)}},
  author = {Moura, Leonardo de and Ullrich, Sebastian},
  journal = {CADE-28 (LNCS 12699), Springer},
  year = {2021},
  url = {https://doi.org/10.1007/978-3-030-79876-5_37}
}

References

7 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. 1. Buzzard, K., Commelin, J., Massot, P.: Formalising Perfectoid Spaces. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 299–312. CPP 2020, New York, NY, USA (2020). https://doi.org/10.1145/3372885.3373830, https://doi.org/10. 1145/3372885.3373830… ↗
  2. Springer International Publishing, Cham (2020) 6. Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP) (Sep 2017). https://doi.org/http://dx.doi.org/10.1145/3110278 7. Jones, S.L.P.: Compiling Haskell by p… — [doi:10.1145/3110278](https://doi.org/10.1145/3110278) find
  3. Springer-Verlag (1996) 8. Miller, D., Nadathur, G.: Programming with Higher-Order Logic. find
  4. Cambridge (2012) 9. de Moura, L., Kong, S., Avigad, J., Van Doorn, F., von Raumer, J.: The Lean theorem prover. In: International Conference on Automated Deduction. pp. 378– 388. find
  5. Springer (2015) 10. Reinking, A., Xie, N., de Moura, L., Leijen, D.: Perceus: Garbage free reference counting with reuse. Tech. Rep. MSR-TR-2020-42, Microsoft Research (2020) 11. Scholze, P.: Liquid tensor experiment. https://xenaproject.wordpress.com/ 2020/12/05/liquid-tensor-experiment (2020), pro… — [arXiv:2001.04301](https://arxiv.org/abs/2001.04301) ↗
  6. CPP 2020, New York, NY, USA (2020). https://doi.org/10.1145/3372885.3373824, https://doi.org/10.1145/3372885. 3373824 14. Ullrich, S., de Moura, L.: Counting immutable beans: Reference counting optimized for purely functional programming. In: 31st Symposium on Implementation and Application of Funct… ↗
  7. Cham (2020) 16. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 60–76. find