Checking a proof again later

Technical version: Proof export and independent checkers

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 proof that Lean accepted today should still be checkable next year, by someone else, with other tools. This page says what Lean keeps once it has checked a file, how a kept proof can be checked again by Lean and by programs written independently of Lean, and why the version of Lean has to be fixed if a check is to be repeated exactly. It ends with the work that keeps proofs usable as Lean and its libraries change.

What Lean keeps

When Lean processes a source file, it saves what the file added to Lean's environment, its table of definitions and theorems, in a compiled file whose name ends in .olean. The values are stored just as they lie in memory, so a later run can load the file directly instead of reading it piece by piece. A file that imports another reads its compiled form; it does not check the other file's proofs again.

That is what makes large libraries practical, and it has a consequence. A theorem imported from a compiled file is believed because it was checked when the compiled file was made. If something went wrong at that moment, nothing later in the same run will notice.

Replaying the proofs

The first way to check again is to replay. A tool now called leanchecker reads the definitions and proofs stored in compiled files and passes them through the Lean kernel once more. It began as a separate program, lean4checker; it was merged into Lean and has shipped with every version of Lean since 4.28.0. With the option --fresh it replays everything from the start, imported files included, which is slower.

Lean's guide to validating proofs says what replaying catches: faults in the way Lean manages the Lean kernel's state, for instance when it works in parallel or handles imports, and programs that add theorems by going around the Lean kernel. It also says what replaying does not catch. The tool uses the same Lean kernel, and it assumes the compiled files themselves are well formed.

Exporting a proof

The second way is to take the proofs out of Lean altogether. A program called lean4export writes chosen definitions and theorems, with everything they depend on, as plain text in a documented format: one record per line, each in JSON. A program that reads this text needs no part of Lean. It sees the proofs exactly as the Lean kernel would, without Lean's parser, its notation or its tactics in between.

Pollack had argued for this arrangement in 1998. A proof can be checked again by a second, simple checker for the same logic, perhaps one whose correctness has been reviewed by experts and tested on earlier proofs; if a few such checkers become trusted, people can keep using whatever tools they like to construct proofs in the first place.

Independent checkers

Several programs check Lean proofs without using the Lean kernel.

Lean4Lean is a checker written in Lean itself. Its author describes it as the first complete checker for Lean 4 apart from the Lean kernel, which is written in C++; it runs between 20 and 50 per cent slower and can check the whole of Mathlib. Because it is written in a language in which things can be proved, properties of the checker can be proved too, and the work has already led to one fault in Lean's checking being found and fixed.

nanoda is a checker written in Rust that reads the files lean4export writes. Lean's guide names it as developed independently, and as one of the checkers its strictest procedure can use.

The Lean Kernel Arena is a site that presents, tests and compares checkers for Lean on a common set of tests. When it was consulted for this page, its table listed the official checker for Lean 4.34.1 beside Lean4Lean, nanoda and many others. Lean's guide points to it for anyone who wants still more confidence.

Agreement between checkers written by different people, in different languages, is evidence of a different kind from a single check. When every one of them must accept, a fault would have to be present in all of them at once to let a false proof through.

Fixing the version

A check can be repeated exactly only with the same version of Lean. A Lean project names the version it uses in a one-line text file called lean-toolchain, kept at the top of the project; the toolchain manager, elan, reads it and runs that version. Lean's reference advises naming an exact version rather than a channel such as stable, so that people working together use the same one and older states of a project can still be checked and tested. The project this wiki records fixes its version of Lean at 4.34.1 (see the move to Lean).

Why proofs need upkeep

A proof, once checked, stays a proof in the logic it was checked in. What wears out is the ability to run the check again with current tools.

New versions of Lean appear every month, and Mathlib, the main library of mathematics, moves with them. The authors of a 2025 paper on Mathlib's maintenance write that code written for one version of Mathlib may no longer compile with a newer one, and that a project which falls too far behind may find it can no longer contribute its results back. To soften this, a theorem that is renamed keeps its old name for a grace period of several months, marked as out of date; anyone who uses the old name gets a warning that names the new one.

The move from Lean 3 to Lean 4 was a change of this kind on a large scale: it meant translating Mathlib into the new language. Notes left during that translation numbered well over 5,000 in the summer of 2023 and roughly 1,500 when that paper was written in 2025. (See Lean 1 to Lean 3 and Lean 4.)

Two practices follow. Keep the exact version with the proof, so that the original check can be repeated. And expect to revise the proof when moving it to a newer version, so that it stays usable by new work.

Next

Stating the right thing turns to the one question no re-check can answer: whether the statement says what was meant.