ValidatingProofs.lean

/-
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Joachim Breitner
-/
import VersoManual

import Manual.Meta

import Verso.Code.External

open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean

set_option pp.rawOnError true
set_option guard_msgs.diff true

open Verso.Code.External (lit)

open Lean (Syntax SourceInfo)

#doc (Manual) "Validating a Lean Proof" =>
%%%
file := "ValidatingProofs"
tag := "validating-proofs"
number := false
htmlSplit := .never
%%%

This section discusses how to validate a proof expressed in Lean.

The steps needed to rule out a misleading proof depend on the author's {deftech}[trust] assumptions towards the _proof author_ (including authors that proved depended-upon theorems), the _verification software_, and the _correctness of the statement_.
Each of these is explained in detail below.

* Regarding the _proof author_, we distinguish whether one is dealing with an {tech}[honest] proof author, and needs protection against only benign mistakes, or a possibly-{tech}[malicious] proof author that actively tries to mislead.

    In particular, we use {deftech}_honest_ when the goal is to create a valid proof.
    This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for proof code that clearly only serves to circumvent the system (such as using the {option}`debug.skipKernelTC`).
    Note that the {keyword}`unsafe` marker on API functions is unrelated to whether this API can be used in an dishonest way.

    In contrast, we use {deftech}_malicious_ to describe proof code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system.
    This includes un-reviewed AI-generated proofs and programs.

* Regarding the verification software, Lean takes {ref "elaboration-compilation"}[a number of steps] to process a theorem and its proof. Some of these steps are part of the {deftech}[trusted computing base] (TCB), which typically comprises at least the Lean {tech}[kernel] or an alternative kernel such as [`nanoda`](https://github.com/ammkrn/nanoda_lib).

* Regarding the correctness of the statement, it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”.
No matter what software is used and how trusted the environment is, a theorem is meaningful only if its author(s) and user(s) are certain that its statement mathematically expresses its intended informal meaning.

    As written, the statement is {tech (key := "Lean elaborator")}[elaborated] before being passed to the {tech}[kernel].
    As such, the {tech (key := "Lean elaborator")}[elaborator] is also part of the {tech (key := "trusted computing base")}[TCB].
    To avoid trusting the {tech (key := "Lean elaborator")}[elaborator], one has to {keywordOf Lean.Parser.Command.print}`#print` the statement with the {keywordOf Lean.Util.PPExt.pp.raw}`pp.raw` option set to `true` to get the elaborated type and manually verify that it indeed expresses the desired statement.
    Unfortunately the raw output is not user-friendly, so including the {tech (key := "Lean elaborator")}[elaborator] in the {tech (key := "trusted computing base")}[TCB] is currently the most reasonable approach.

Below, an escalating sequence of checks are presented, with instructions on how to perform them, an explanation of what they entail and the mistakes or attacks they guard against.
To avoid repetition, we will not discuss trust towards the correctness of the statement every time.

# The Blue Double Check Marks
%%%
tag := "validating-blue-check-marks"
%%%

In regular everyday use of Lean, it suffices to check the blue double check marks next to the theorem statement for assurance that the theorem is proved.

## Instructions

While working interactively with Lean, once the theorem is proved, blue double check marks appear in the gutter to the left of the code.

:::figure "A double blue check mark"
![A theorem with double blue check marks appearing in the editor gutter](/static/screenshots/doublecheckmarks.png)
:::

## Significance

The blue ticks indicate that the theorem statement has been successfully elaborated, according to the syntax and type class instances defined in the current file and its imports, and that the Lean {tech}[kernel] has accepted a proof of that theorem statement that follows from the definitions, theorems and axioms declared in the current file and its imports.

## Trust

This check is meaningful if one trusts the authors of the imported libraries to be {tech}[honest], that they checked that the theorems in their libraries express their intended informal meanings, and that no unsound axioms have been declared and used.

## Protection

:::listBullet "🛡️"
This check protects against

* Incomplete proof (missing goals, tactic error) *of the current theorem*
* Explicit use of {lean}`sorry` *in the current theorem*
* {tech}[Honest] bugs in meta-programs and tactics
* Proofs still being checked in the background
:::

## Comments

In the Visual Studio Code extension settings, the symbol can be changed.
Editors other than VS Code may have a different indication.

Running {lake}`build`{lit}` +Module`, where {lit}`Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees.

# Printing Axioms
%%%
tag := "validating-printing-axioms"
%%%

The blue double check marks appear  even when there are explicit uses of {lean}`sorry` or incomplete proofs in the dependencies of the theorem.
Because both {lean}`sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on.

## Instructions

:::keepEnv
```lean -show
inductive TheoremStatement : Prop where | intro
theorem thmName : TheoremStatement := .intro
```

Write {leanCommand}`#print axioms thmName` after the theorem declaration, with {lean}`thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound`.

:::

## Significance

This command prints the set of axioms used by the theorem and the theorems it depends on.
The three axioms above are standard axioms of Lean's logic, and benign.

* If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses {lean}`sorry` or is otherwise incomplete.
* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion.
* Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms.

## Trust

This check is meaningful if one trusts the authors of the imported libraries to be {tech}[honest].

## Protection

:::listBullet "🛡️"
(In addition to the list above)

* Incomplete proofs
* Explicit use of {lean}`sorry`
* Custom axioms
:::

# Re-Checking Proofs with `lean4checker`
%%%
tag := "validating-lean4checker"
%%%

There is a small class of bugs and some dishonest ways of presenting proofs that can be caught by re-checking the proofs that are stored in {tech}[`.olean` files] when building the project.

## Instructions

Build your project using {lake}`build`, run `lean4checker --fresh` on the module that contains the theorem of interest, and check that no error is reported.

## Significance

The `lean4checker` tool reads the declarations and proofs as they are stored by `lean` during building (the {tech}[`.olean` files]), and replays them through the {tech}[kernel].
It trusts that the {tech}[`.olean` files] are structurally correct.

## Trust

This check is meaningful if one believes the authors of the imported libraries to not be very cunningly {tech}[malicious], and to neither compromise the user’s system nor use Lean’s extensibility to change the interpretation of the theorem statement.

## Protection

:::listBullet "🛡️"
(In addition to the list above)

* Bugs in Lean’s core handling of the {tech}[kernel]’s state (e.g. due to parallel proof processing, or import handling)
* Meta-programs or tactics intentionally bypassing that state (e.g. using low-level functionality to add unchecked theorems)
:::

## Comments

Since `lean4checker` reads the {tech}[`.olean` files] without validating their format, this check is  prone to an attacker crafting invalid `.olean` files (e.g. invalid pointers, invalid data in strings).

Lean tactics and other meta-code can perform arbitrary actions when run.
Importing libraries created by a determined {tech}[malicious] attacker and building them without further protection can compromise the user's system, after which no further meaningful checks are possible.

We recommend running `lean4checker` as part of CI for the additional protection against bugs in Lean's handling of declaration and as a deterrent against simple attacks.
The [lean-action](https://github.com/leanprover/lean-action) GitHub Action provides this functionality by setting `lean4checker: true`.

Without the `--fresh` flag the tool can be instructed to only check some modules, and assume others to be correct (e.g. trusted libraries), for faster processing.

# Gold Standard: `comparator` and external checkers
%%%
tag := "validating-comparator"
%%%

To protect against a seriously {tech}[malicious] proof compromising how Lean interprets a theorem statement or the user's system, additional steps are necessary.
This should only be necessary for high risk scenarios (proof marketplaces, high-reward proof competitions, unaligned AI).

## Instructions

In a trusted environment, write the theorem *statement* (the “challenge”), and then feed the challenge as well as the proposed proof to the [`comparator`](https://github.com/leanprover/comparator) tool, with external checkers enabled, as documented there.

## Significance

Comparator will build the proof in a sandboxed environment, to protect against {tech}[malicious] code in the build step.
The proof term is exported to a serialized format.
Outside the sandbox and out of the reach of possibly malicious code, it validates the exported format, replays the proofs using both Lean's {tech}[kernel] and/or an external checker and also ensures that the proved theorem statements match those in the trusted challenge file.

## Trust

This check is meaningful if the theorem statement in the trusted challenge file is correct and the sandbox used to build the possibly-{tech}[malicious] code is safe.

## Protection

:::listBullet "🛡️"
(In addition to the list above)

* Actively {tech}[malicious] proofs
* Implementation bugs present in some (but not simulatenously in all) of the used checkers.
:::

## Comments

At the time of writing, `comparator` supports using the official Lean {tech}[kernel] and the external checker [`nanoda`](https://github.com/ammkrn/nanoda_lib), which is developed independently and implemented in Rust. The [Lean Kernel Arena](https://arena.lean-lang.org/) features more external checkers that can be used manually for even more confidence.

# Remaining Issues

When following the gold standard of checking proofs using comparator, some assumptions remain:

* The soundness of Lean’s logic.
* The plumbing provided by the `comparator` tool is correct.
* The sandbox used by `comparator` is secure.
* There is no implementation bug affecting all of the used checkers simultaneously.
* No human error or misleading presentation of the theorem statement in the trusted challenge file.

  If there are doubts that the theorem means what it appears to mean, its statement and all referenced definitions must be investigated carefully, in particular with regard to custom notation and type classes.
  Some external checkers offer raw pretty-printing capabilities that are not affected by changes to parser or notation in the source file.

# On `Lean.trustCompiler` (up to Lean 4.28.0)
%%%
tag := "validating-trustCompiler"
%%%

Lean supports proofs by native evaluation.
This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the {tech}[kernel].

Specific uses wrapped in {tech}[honest] tactics (e.g. {tactic}`bv_decide`) are generally trustworthy.
The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted.

General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the {tech}[kernel]'s evaluation.
In particular, for every {attr}`implemented_by`/{attr}`extern` attribute in libraries it becomes part of the trusted code base that the replacement is semantically equivalent.

All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler.
When that level of checking is needed, proofs have to avoid using native evaluation.

Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use {name}`Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The {name}`Lean.trustCompiler` machinery is deprecated and will eventually be removed.