PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:20Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Proof export and independent checkers}}		{{DISPLAYTITLE:Proof export and independent checkers}}
	{{Plebeian\|Lean theorem prover/Explainers/Checking a proof again later}}		{{Plebeian\|Lean theorem prover/Explainers/Checking a proof again later}}
			{{Lean theorem prover map}}

	When a Lean source file is elaborated, the Lean kernel checks every definition and theorem		When a Lean source file is elaborated, the Lean kernel checks every definition and theorem

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:10Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Proof export and independent checkers}}
{{Plebeian|Lean theorem prover/Explainers/Checking a proof again later}}

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
<code>leanchecker</code>, 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.<ref name="rm-vp">"Validating a Lean Proof", a chapter of ''The Lean Language Reference'' (edition covering Lean 4.34.0), with its sections "The Blue Double Check Marks", "Printing Axioms", "Re-Checking Proofs with lean4checker", "Gold Standard: comparator and external checkers", "Remaining Issues" and "On Lean.trustCompiler (up to Lean 4.28.0)". [https://lean-lang.org/doc/reference/4.34.0/ValidatingProofs/ lean-lang.org/doc/reference/4.34.0/ValidatingProofs/]</ref>

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
<code>sorry</code> 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.<ref name="rm-vp" /> The checks below remove some of these
assumptions.

== Listing the axioms ==

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

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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
</pre>

Lean warns <code>declaration uses `sorry`</code> at the third theorem, and prints:

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">'two_add_two' does not depend on any axioms
'em_or' depends on axioms: [propext, Classical.choice, Quot.sound]
'unfinished' depends on axioms: [sorryAx]</pre>

<code>propext</code>, <code>Classical.choice</code> and <code>Quot.sound</code> are Lean's
three standard axioms (see [[Lean theorem prover/Foundations/The three axioms|the three
axioms]]). <code>sorryAx</code> marks a gap: a <code>sorry</code> or an incomplete proof
somewhere in the dependencies, which the editor's mark next to the theorem does not
reveal.<ref name="rm-vp" />

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

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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
</pre>

Everything is accepted, and the last line prints

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">'oops' depends on axioms: [propext, Quot.sound, ident_five_zero._native.decide.ax_1_1]</pre>

<code>decide +native</code> 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,
<code>Lean.trustCompiler</code>.<ref name="rm-vp" /> Any axiom other than the standard three
means that the proof depends on something the Lean kernel did not check.

<code>#print axioms</code> 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 <code>.olean</code> 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, <code>debug.skipKernelTC</code>, that skips the check.<ref name="rm-vp" /> The
following file uses it together with the false tactic from [[Lean theorem prover/System/Metaprogramming in Lean|metaprogramming in
Lean]], which the Lean kernel would reject.

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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
</pre>

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

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">ℹ [2/3] Built Hack (868ms)
info: Hack.lean:12:0: 'bad' does not depend on any axioms
Build completed successfully (3 jobs).</pre>

The reference manual names <code>debug.skipKernelTC</code> as an example of code whose only
purpose is to circumvent the system.<ref name="rm-vp" /> The second check exists for this
case. '''<code>leanchecker</code>''', which is part of the Lean 4.34.1 toolchain, reads the
<code>.olean</code> files and replays every definition and theorem in them through the Lean
kernel.<ref name="rm-bt">"Build Tools and Distribution", a chapter of ''The Lean Language Reference'' (edition covering Lean 4.34.0). [https://lean-lang.org/doc/reference/4.34.0/Build-Tools-and-Distribution/ lean-lang.org/doc/reference/4.34.0/Build-Tools-and-Distribution/]</ref>
Since Lean 4.28.0 the program is the external checker <code>lean4checker</code>, shipped with
every toolchain;<ref name="rn428">"Lean 4.28.0", in "Release Notes", ''The Lean Language Reference'' (edition covering Lean 4.34.0), section "External Checker". [https://lean-lang.org/doc/reference/4.34.0/releases/v4.28.0/ lean-lang.org/doc/reference/4.34.0/releases/v4.28.0/]</ref>
the reference manual's chapter on validating proofs still calls it by that
name.<ref name="rm-vp" /> Run as <code>lake env leanchecker --fresh
Hack</code>, it reports:

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">uncaught exception: while replaying declaration 'bad':
(kernel) declaration type mismatch, 'bad' has type
True
but it is expected to have type
False</pre>

and exits with a failure. With <code>--fresh</code> 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.<ref name="rm-vp" /><ref name="l4l" />

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 <code>.olean</code>
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.<ref name="rm-vp" /> 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.<ref name="res-export">"lean4export", Reservoir, the index of Lake packages: "A simple declaration exporter for Lean 4 using the Lean 4 NDJSON export format". [https://reservoir.lean-lang.org/@leanprover/lean4export reservoir.lean-lang.org/@leanprover/lean4export]</ref>
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.<ref name="arena-tut">"Tutorial" test suite, Lean Kernel Arena. [https://arena.lean-lang.org/tutorial/ arena.lean-lang.org/tutorial/]</ref>

== Independent checkers ==

Three programs illustrate the range.

'''nanoda''' is a checker for Lean exports written in Rust, developed independently of
Lean.<ref name="rm-vp" /><ref name="arena-nanoda">"nanoda", checker page, Lean Kernel Arena. [https://arena.lean-lang.org/checker/nanoda/ arena.lean-lang.org/checker/nanoda/]</ref>
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 <code>.olean</code> 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.<ref name="l4l">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, 2:1–2:23. doi:[https://doi.org/10.4230/LIPIcs.TYPES.2025.2 10.4230/LIPIcs.TYPES.2025.2]; full version [https://arxiv.org/abs/2403.14064 arXiv:2403.14064].</ref>
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".<ref name="arena-l4l">"lean4lean", checker page, Lean Kernel Arena. [https://arena.lean-lang.org/checker/lean4lean arena.lean-lang.org/checker/lean4lean]</ref>

'''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.<ref name="rm-vp" />

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.<ref name="arena">Lean Kernel Arena: "presents, tests and benchmarks proof checkers for the Lean Theorem Prover". [https://arena.lean-lang.org arena.lean-lang.org]</ref><ref name="arena-tut" />

== What each check guards against ==

{| class="wikitable"
! Check !! Reads !! Guards against !! Does not guard against
|-
| Editor or Lake build || source files || incomplete proofs, <code>sorry</code> in the theorem, honest bugs in tactics || gaps in dependencies, extra axioms, bypassed checks
|-
| <code>#print axioms</code> || Lean's environment in memory || <code>sorry</code> anywhere in the dependencies, custom axioms, native computation || constants that were never checked
|-
| <code>leanchecker</code> || <code>.olean</code> files || constants added without the Lean kernel's check, bugs in handling the Lean kernel's state || crafted <code>.olean</code> 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,<ref name="rm-vp" /> 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.<ref name="l4l" /> 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.<ref name="rm-vp" /> That question is
taken up in [[Lean theorem prover/Explainers/Stating the right thing|stating the right thing]].

== Next ==

[[Lean theorem prover/System/Monads and do-notation|Monads and do-notation]] returns to Lean
as a programming language.

== References ==

<references />

Lean theorem prover/System/Proof export and independent checkers - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source