2026-09-30
Microsoft Research and KIT reimplement Lean in Lean and emit C. Hygienic macros, tabled typeclasses, and FBIP drop Lean 3's C++ wall and the interpreter tax on tactics.
Lean 3 scaled because it was extensible. Starting in 2017 the community built mathlib on it. At the time of this paper the library was about 500k lines, with Schemes, perfectoid spaces, and the scaffolding for Peter Scholze's Liquid Tensor challenge. mathlib also ships metaprograms: a ring solver, a Presburger decision procedure, semantic linters. Galois used Lean 3 metaprograms for a SQL query equivalence checker.
Two walls. Parser, elaborator, and code generator lived in C++; users could not touch them without patching the system. Proof automation written as Lean 3 metaprograms ran on a VM and could not match C++ or OCaml implementations of the same procedures.
Lean 4 is a reimplementation of the prover in Lean, and a compiled functional language. It was open-sourced in early 2021.
Four design choices.
Hygienic macros. Lean 3 syntax extension was restrictive "syntax sugar" substitution; the tactic language also suffered accidental name capture. Lean 4 takes capture-avoiding macros from the Scheme family and rebuilds them for interactive theorem provers. Users see a tower: infix expands to notation, which expands to macro, which splits into a syntax declaration plus macrorules. Stop at the level that fits, or drop to procedural macros. Parsing is separated from expansion, so tools get a concrete syntax tree before macros fire: completion, go-to-definition, refactoring. A Boolean-expression DSL is the running example: [BExpr| p ∨ true] becomes constructor applications.
Tabled typeclass resolution. Heavy typeclass use in mathlib exposed two Lean 3 failures: no term indexing, so extra overhead, and exponential blow-up on diamonds. The new solver treats instances as λ-Prolog Horn clauses, indexes them with discrimination trees, and tables (memoizes) repeating goals. The code lives in SynthInstance and DiscrTree.
Code generation. The compiler applies GHC-style transformations, but Lean is strict. @[inline] and @[specialize] strip abstraction towers. Proofs are erased, then the term becomes IR. The default backend emits C; IR is itself a Lean datatype, so other backends can be written in Lean. An IR interpreter runs from the editor; calls into ahead-of-time native code skip interpretation, so the tax is small if expensive tactics are precompiled.
Memory uses reference counting. The resurrection hypothesis: in functional updates, an object often dies just before an object of the same kind is allocated. When the count is one, mutate in place. That style is functional but in-place (FBIP). map f as allocates nothing if as is unshared; map (map inc) as also allocates nothing on an unshared list of integer lists. Unlike static linearity, a shared prefix still leaves the unshared tail free to reuse. Arrays and hash tables can therefore live in pure code, which is what decision procedures actually want.
Tactics and the elaborator are Lean programs. simp is one of mathlib's most used tactics; users can change it. The LSP server is incremental, built on the standard library's task abstraction. VS Code is the preferred editor.
This is a system description. There is no head-to-head proving benchmark against Lean 3, Coq, or Isabelle in the paper.
| Item | Number / fact | Baseline |
| Project start | 2013, Calculus of Inductive Constructions | Lean 1/2/3 lineage |
| Lean 4 release | early 2021, open source | rewritten in Lean |
| mathlib at the time | 500k lines | still Lean 3, port in progress |
| map on unshared list | zero allocations | ordinary functional allocation |
| FBIP vs ocamlopt / GHC | "often outperforms", authors' preliminary claim | numbers live in Perceus and Counting immutable beans, not here |
Three early applications: Galois's Reopt translation verifier, a package for inductive-inductive types, a self-balancing car controller. No port-completion figure for mathlib.
People who write tactics get a real path: automation compiles to C and loads as a plugin. Parser, elaborator, pretty printer, and code generator are no longer C++ only.
FBIP is the paper's concrete answer to whether pure functional code can be fast. Decision procedures want hash tables. Linear types ask you to prove unsharing in the type system; reference counting checks it at run time: mutate if unique, copy if shared. The cost is bookkeeping.
Hygienic macros turn ITP syntax extension from one more ad hoc sugar into a composable tower. Later notation-heavy libraries and embedded DSLs sit on that tower. Read this as a design document, not a bake-off.
The authors call this a long-term effort. The roadmap at publication included SMT and first-order prover integration, extra compiler backends, and porting Lean 3 mathlib plus the widget library. None of that was done in early 2021.
Almost no system-level evaluation. The claim that tabled resolution kills diamond blow-up is detailed in Selsam, Ullrich, and de Moura's Tabled typeclass resolution. FBIP speed numbers are in the Perceus technical report and the IFL 2019 paper Counting immutable beans. This paper alone cannot tell you how much faster, on which programs.
The trusted kernel stays relatively small, while macros, elaborator, and tactics become a large extension surface. A buggy extension does not corrupt the kernel, but it does corrupt the proof state the user sees. The paper does not discuss how extension authors keep a wrong elaboration from looking like a proof.
The resurrection hypothesis is an empirical observation, not a theorem. When data is mostly shared, FBIP falls back to ordinary allocation.