Lean theorem prover/System/The compiler and runtime

Plain-language version: Programs and proofs in one language

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

A Lean definition is used in two ways. The Lean kernel checks it as a term of the type theory, and the compiler turns it into machine code that runs. The two paths start from the same definition and, except in the cases described at the end of this page, do not meet again. This page follows the second path in Lean 4.34.1: from a definition through the compiler's intermediate representations to C, the run-time system's reference counting and its updates in place, the attributes that let compiled code differ from the definition the Lean kernel sees, and what all of this adds to what has to be trusted.

Two consumers of one definition

When a definition is elaborated, the result goes two ways. The compiler receives it with its recursion intact; the Lean kernel receives a version in which recursion has been expressed through recursors or well-founded recursion and can be checked. Before generating code, the compiler erases proofs, which have no run-time content. The compiled code is never shown to the Lean kernel. A theorem about a function is a theorem about the definition; that the machine code computes the same function is a property of the compiler, not something the Lean kernel has checked.

From definitions to C

Lean's notes for version 4.22.0, of 14 August 2025, state that "the old compiler has been replaced by the new compiler". In 4.34.1 that compiler, written in Lean, is the one in use. It works in stages:

1. The elaborated definition is translated into LCNF, the Lean Compiler Normal Form, a representation in A-normal form in which every intermediate result is bound to a name.
2. Later passes, still over LCNF, make allocation, reference-count updates and memory reuse explicit instructions. The result is also translated into the compiler's IR, the form that Lean prints on request (below).
3. The same result is emitted as C. Each Lean module becomes a C file, which a C compiler shipped with Lean compiles to native code.

When Lean evaluates code while processing a file, as #eval does, an interpreter runs the IR, and switches to native code for any function that has been compiled ahead of time, which includes the standard library.

The IR of a definition can be printed. This function adds one to every element of a list.

set_option trace.compiler.ir.result true in
def incAll : List Nat → List Nat
  | [] => []
  | x :: xs => (x + 1) :: incAll xs

Lean 4.34.1 prints:

[Compiler.IR] [result]
    def incAll (x_1 : tobj) : tobj :=
      case x_1 : tobj of
      List.nil →
        ret x_1
      List.cons →
        let x_2 : tobj := proj[0] x_1;
        let x_3 : tobj := proj[1] x_1;
        block_4 (x_5 : tobj) (x_6 : u8) :=
          let x_7 : tagged := 1;
          let x_8 : tobj := Nat.add x_2 x_7;
          dec x_2;
          let x_9 : tobj := incAll x_3;
          block_10 (x_11 : obj) :=
            ret x_11;
          case x_6 : u8 of
          Bool.false →
            set x_5[1] := x_9;
            set x_5[0] := x_8;
            jmp block_10 x_5
          Bool.true →
            let x_12 : obj := ctor_1[List.cons] x_8 x_9;
            jmp block_10 x_12;
        let x_13 : u8 := isShared x_1;
        case x_13 : u8 of
        Bool.false →
          jmp block_4 x_1 x_13
        Bool.true →
          inc x_3;
          inc x_2;
          dec x_1;
          jmp block_4 ◾ x_13

The same definition, given to lean -c, yields a C function. In an excerpt, the test, the call to the C implementation of addition and the two ways of producing the new cell read:

v_isSharedCheck_13_ = !lean_is_exclusive(v_x_1_);
…
v___x_8_ = lean_nat_add(v_head_2_, v___x_7_);
…
if (v_isShared_6_ == 0)
{
lean_ctor_set(v___x_5_, 1, v___x_9_);
lean_ctor_set(v___x_5_, 0, v___x_8_);
…
v_reuseFailAlloc_12_ = lean_alloc_ctor(1, 2, 0);

Reference counting and update in place

Lean manages memory by reference counting. Every object on the heap carries a count of the references to it; the count rises when a reference is copied and falls when one is dropped, and an object whose count reaches zero is freed at once. The traditional objection to reference counting in functional languages is its cost. Ullrich and de Moura's answer is that an exact count is also information: it says whether a value is shared, and a value that is not shared may be changed in place without any observer being able to tell.

The IR above shows the mechanism. isShared x_1 tests the count of the incoming list cell. If the cell is not shared, the branch Bool.false overwrites its two fields with set and returns the same cell: the old list is updated in place. If it is shared, ctor_1[List.cons] allocates a new cell and the old one is left for its other owners. In the paper this pair of steps is a reset instruction, which drops an unshared value's references to its fields but keeps its cell, followed by reuse, which places the new constructor in that cell. The authors observe that many objects die just before an object of the same kind is created, which they call the resurrection hypothesis, and that a function such as map applied to an unshared list therefore allocates no memory at all. In the Lean 4 system description this is presented as a programming style, functional but in place: code is written as pure functions, and runs with destructive updates wherever values are not shared.

Arrays and strings follow the same rule. Their primitive operations modify the value in place when they hold the only reference, and copy it otherwise. Two further techniques keep the cost down. Borrowed parameters, which a function uses without consuming, need no count updates, and the compiler infers many of them; and values reachable from only one thread use cheaper, unsynchronised count updates. Reference counting cannot reclaim cycles, but the part of Lean that can be reasoned about cannot create cyclic data, so the runtime has no cycle collector.

Code that differs from its definition

Two attributes let the code that runs differ from the definition that the Lean kernel checks.

@[extern "sym"] binds a definition to a C symbol: compiled code calls the C function sym instead of code generated from the definition. Addition of natural numbers is an example. The definition of Nat.add, the one theorems are about, is by recursion on the unary representation (zero and successor); compiled code calls lean_nat_add, as in the C above. At run time a natural number is either a small value stored directly in the machine word or a pointer to a multi-precision number. Lean reports the binding:

import Lean
open Lean

#eval show CoreM (Option String) from do
  return getExternNameFor (← getEnv) `c ``Nat.add

This prints some "lean_nat_add".

@[implemented_by f] replaces a definition by another Lean function f in compiled code. Lean's own documentation of the attribute states that "the provided implementation is not checked to be equivalent to the original definition". Nothing prevents a wrong one.

def alwaysZero (_ : Nat) : Nat := 0

@[implemented_by alwaysZero]
def ident (n : Nat) : Nat := n

#eval ident 5

theorem ident_five : ident 5 = 5 := rfl

#eval prints 0, and the theorem that ident 5 = 5 is accepted. Both are correct by their own lights: #eval ran the code the compiler was told to use, and the Lean kernel checked the definition. The most common uses, according to the same documentation, are to give an efficient unsafe implementation of a function whose definition is simple to reason about, and to make an unsafe function callable from safe code. A safer variant, @[csimp], makes the same substitution only on the strength of a proved equation between the two functions.

What it adds to what has to be trusted

For a proof, ordinarily nothing. Apart from one deprecated primitive, Lean.reduceBool, whose use #print axioms reports as the axiom Lean.trustCompiler, the Lean kernel never runs compiled code, so neither the compiler nor any @[extern] or @[implemented_by] annotation is consulted when a theorem is checked. The theorem ident_five above holds whatever the compiled code does.

For a program, everything above is trusted: the compiler, the C compiler, the runtime, and the claim behind every @[extern] and @[implemented_by] that the code computes what the definition says. A proof about a function is a proof about the definition.

The two meet in one place. Some tactics, such as decide +native and bv_decide, prove a statement by running compiled code and admitting its result. Such a proof depends on the compiler and on every @[extern] and @[implemented_by] on the path, and can be wrong when the compiled code disagrees with the definition. Since Lean 4.29.0 each such computation introduces its own axiom, which #print axioms lists, so the dependence is visible. Proof export and independent checkers shows the function ident above used to prove a falsehood in exactly this way, and how the axiom gives it away.

Next

Lake and Lean projects describes how Lean source files are organised into Lake packages and compiled together.