Lean theorem prover/System/Proof export and independent checkers

Plain-language version: Checking a proof again later

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

When a Lean source file is elaborated, the Lean kernel checks every definition and theorem before it enters Lean's environment, its table of definitions and theorems. That first check happens inside the same program that parsed the file, ran its tactics and executed whatever code the file and its imports contain. This page is about checking again: listing the axioms a theorem depends on, replaying compiled results through the Lean kernel with leanchecker, exporting proofs to a file, and checking that file with checkers written independently of Lean. For each, it says what the check guards against and what it does not. The examples were run with Lean 4.34.1.

What the first check leaves open

Lean's reference manual sets out an escalating series of checks and distinguishes two situations. In the honest case the author is trying to produce a valid proof and the risks are mistakes and bugs. In the malicious case someone is trying to mislead: by exploiting bugs, by code that circumvents the system, or by compromising the machine; the manual counts unreviewed proofs generated by AI in this case. It also separates two questions: whether a theorem has a valid proof, and what the theorem's statement means.

The ordinary check, a theorem accepted in the editor or a Lake build of its Lean module without errors or warnings, protects against incomplete proofs, an explicit sorry in the theorem itself and honest bugs in tactics and other metaprograms. It assumes that the statement says what is intended, that the authors of imported libraries are honest, and that no unsound axiom has been declared and used. The checks below remove some of these assumptions.

Listing the axioms

#print axioms lists every axiom a theorem depends on, directly or through the theorems it uses.

theorem two_add_two : 2 + 2 = 4 := rfl

theorem em_or (p : Prop) : p ∨ ¬p := Classical.em p

theorem unfinished : 2 + 2 = 5 := sorry

#print axioms two_add_two
#print axioms em_or
#print axioms unfinished

Lean warns declaration uses `sorry` at the third theorem, and prints:

'two_add_two' does not depend on any axioms
'em_or' depends on axioms: [propext, Classical.choice, Quot.sound]
'unfinished' depends on axioms: [sorryAx]

propext, Classical.choice and Quot.sound are Lean's three standard axioms (see the three axioms). sorryAx marks a gap: a sorry or an incomplete proof somewhere in the dependencies, which the editor's mark next to the theorem does not reveal.

The command also exposes proofs that rest on running compiled code. The page on the compiler and runtime defines a function whose compiled code, supplied through @[implemented_by], disagrees with its definition. A tactic that trusts compiled code can then prove a falsehood:

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

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

theorem ident_five : ident 5 = 5 := rfl

theorem ident_five_zero : ident 5 = 0 := by decide +native

theorem oops : False := by
  have h1 := ident_five
  have h2 := ident_five_zero
  omega

#print axioms oops

Everything is accepted, and the last line prints

'oops' depends on axioms: [propext, Quot.sound, ident_five_zero._native.decide.ax_1_1]

decide +native evaluated the claim with compiled code and admitted the result as a new axiom. Since Lean 4.29.0 each such computation has its own axiom, named after the theorem that made it; before that, all of them appeared as one axiom, Lean.trustCompiler. Any axiom other than the standard three means that the proof depends on something the Lean kernel did not check.

#print axioms reads Lean's environment as it stands. It cannot detect a theorem that entered that table without being checked at all.

Replaying through the Lean kernel: leanchecker

Lean's environment is held in memory while a file is processed and saved, Lean module by Lean module, in .olean files. Code run during elaboration has the access it needs to add a constant to that table without passing it to the Lean kernel, and Lean has a debugging option, debug.skipKernelTC, that skips the check. The following file uses it together with the false tactic from metaprogramming in Lean, which the Lean kernel would reject.

import Lean
open Lean Elab Tactic

elab "cheat" : tactic => do
  let goal ← getMainGoal
  goal.assign (mkConst ``True.intro)
  replaceMainGoal []

set_option debug.skipKernelTC true in
theorem bad : False := by cheat

#print axioms bad

As the library Hack of a small Lake package, it compiles without error, and the axiom check reports nothing amiss:

ℹ [2/3] Built Hack (868ms)
info: Hack.lean:12:0: 'bad' does not depend on any axioms
Build completed successfully (3 jobs).

The reference manual names debug.skipKernelTC as an example of code whose only purpose is to circumvent the system. The second check exists for this case. leanchecker, which is part of the Lean 4.34.1 toolchain, reads the .olean files and replays every definition and theorem in them through the Lean kernel. Since Lean 4.28.0 the program is the external checker lean4checker, shipped with every toolchain; the reference manual's chapter on validating proofs still calls it by that name. Run as lake env leanchecker --fresh Hack, it reports:

uncaught exception: while replaying declaration 'bad':
(kernel) declaration type mismatch, 'bad' has type
  True
but it is expected to have type
  False

and exits with a failure. With --fresh it replays the named Lean module and everything it imports into an empty table; without it, it replays only the Lean module's own constants on top of its imports.

According to the reference manual, this check protects against bugs in Lean's handling of the Lean kernel's state, for instance in parallel processing or imports, and against metaprograms that deliberately bypass that state. It trusts that the .olean files are well formed, and a crafted file could defeat it. It also runs after the code under test has been compiled, and such code, the manual warns, can perform arbitrary actions when run; a determined attacker can compromise the machine before any check takes place. And it uses the same Lean kernel, so it cannot find a bug in the Lean kernel itself.

Exporting proofs

The next step separates the proof from the program that produced it. lean4export writes the constants of a Lean module and everything it depends on to a file in an NDJSON format, one JSON record per line. The file contains terms of the type theory and nothing else: no tactics, no notation, no elaborator. A checker that reads it needs to implement only the type theory: universes, dependent function types, inductive types and their recursors, quotients and definitional equality. It need not trust what the file says about derived data. A test in the Lean Kernel Arena makes the point that a checker "must not blindly trust the recursors it is handed", and should either check them or derive them anew from the inductive type itself.

Independent checkers

Three programs illustrate the range.

nanoda is a checker for Lean exports written in Rust, developed independently of Lean. A bug would have to occur in both nanoda and the Lean kernel, written separately in different languages, to let a false theorem through both.

Lean4Lean, by Mario Carneiro, is a type checker for Lean 4 written in Lean. It reads compiled .olean files, offers the same interface as lean4checker, and can check the whole of Mathlib, running 20 to 50 per cent slower than the Lean kernel, which is written in C++. Because it is written in a language with proofs, parts of it can be, and have been, proved correct against a formalisation of Lean's type theory; that work found a soundness bug in the Lean kernel, which has since been fixed. Its description in the Lean Kernel Arena notes the limit of the approach: it follows the C++ implementation closely, and so "likely shares some implementation bugs with it".

comparator is the reference manual's "gold standard" for high-risk settings; the manual names proof marketplaces, competitions with high rewards, and unaligned AI. The theorem statement is written first, in a trusted setting, as a challenge file. comparator compiles the proposed proof inside a sandbox, exports it, and, outside the sandbox, validates the export, replays it with the Lean kernel, nanoda or both, and checks that the proved statements are exactly those in the challenge file.

The Lean Kernel Arena tests such checkers side by side. It runs each on the same exported tests, some of which a correct checker must accept and some of which it must reject, and publishes the results; the Lean kernel of version 4.34.1 is among the checkers listed.

What each check guards against

Check	Reads	Guards against	Does not guard against
Editor or Lake build	source files	incomplete proofs, sorry in the theorem, honest bugs in tactics	gaps in dependencies, extra axioms, bypassed checks
#print axioms	Lean's environment in memory	sorry anywhere in the dependencies, custom axioms, native computation	constants that were never checked
leanchecker	.olean files	constants added without the Lean kernel's check, bugs in handling the Lean kernel's state	crafted .olean files, a compromised machine, bugs in the Lean kernel
comparator with an external checker	an export, outside a sandbox	malicious proofs, a bug present in one checker but not all	a bug shared by every checker, an unsound logic, a wrong statement

Sources: the reference manual's chapter on validating proofs, and the demonstrations above.

Why check outside the tool that made the proof

The Lean kernel is small, but it is a program, and programs have bugs. Lean 4's kernel was extended for performance, with fast arithmetic on natural numbers, nested inductive types and primitive projections among other things, and Carneiro reports that some soundness bugs entered in the process. A second implementation does not make a bug impossible. It makes a bug matter only if every implementation has it.

There is a second reason. Elaboration runs code, much of it written by users, with the full rights of a program. A check that runs in the same process, on the same machine, after that code, inherits whatever that code did. A check that reads an exported file elsewhere depends only on the file and on the checker.

The checks do not answer the other question, whether the statement means what it is taken to mean. The reference manual lists among the assumptions that remain even at its gold standard: the soundness of Lean's logic, the correctness of the tools and the sandbox, the absence of a bug shared by all checkers, and a statement free of human error, with custom notation and type classes named as places to look. That question is taken up in stating the right thing.

Next

Monads and do-notation returns to Lean as a programming language.