Lean theorem prover/Explainers/Computation inside proofs

Technical version: Definitional equality· Decision procedures

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

Some statements are proved by calculating. That 2 + 2 is 4, or that 97 is prime, can be settled by working the sum or by trying every divisor. Lean accepts such calculations as proofs. This page shows how, what has to be trusted when it does, and what the calculation costs.

A sum as a proof

example : 2 + 2 = 4 := rfl

example : 2 ^ 100 = 1267650600228229401496703205376 := rfl

The proof rfl says that the two sides are the same thing. To accept it, Lean works out both sides and compares the results. Two expressions that compute to the same value are, in Lean's terms, definitionally equal, and for them rfl is a complete proof (see two kinds of equality).

The second line raises 2 to the power 100 and is accepted at once. In the logic a natural number is zero followed by a chain of successors, and a chain of that length could never be written out. The Lean kernel does not try. It stores number literals in a fast library for arithmetic on large numbers, usually GMP, and replaces addition, multiplication and the other basic operations with routines from that library. The Lean Language Reference adds the condition that comes with the speed: these routines are part of the Lean kernel, so if they did not agree with the definitions they stand in for, soundness could suffer.

Deciding a finite question

A finite question can be answered by a program, and the run of the program can be a proof. Here is a test for primality by trial division, applied to 97:

def isPrime (n : Nat) : Bool :=
  n ≥ 2 && (List.range (n - 2)).all (fun k => n % (k + 2) != 0)

#eval isPrime 97

theorem prime97 : isPrime 97 = true := by decide

#print axioms prime97

The function checks that n is at least 2 and that no number from 2 to n − 1 divides it. #eval runs it and prints true. That is a program's answer, not yet a proof. The theorem turns it into one. The tactic decide finds a procedure that decides the statement and evaluates it inside the logic; when the result is "true", that evaluation is the proof, and the Lean kernel repeats it when it checks the theorem. The last line confirms that nothing extra was assumed: 'prime97' does not depend on any axioms.

Running the program instead: native_decide

The same question can be answered faster by running the program as a program and accepting its answer:

theorem prime97_native : isPrime 97 = true := by native_decide

#print axioms prime97_native
#print prime97_native._native.native_decide.ax_1_1

Lean 4.34.1 answers:

'prime97_native' depends on axioms: [prime97_native._native.native_decide.ax_1_1]
axiom prime97_native._native.native_decide.ax_1_1 : decide (isPrime 97 = true) = true

The theorem now rests on an axiom made for the occasion. native_decide evaluated the question the way #eval does, and then added an axiom stating the answer. The Lean kernel asks for no proof of an axiom; it accepts it. So the theorem is only as sound as the evaluation behind the axiom, which means the Lean compiler and every function that has been given a faster implementation for running. The reference manual says that this adds the entire Lean compiler to the trusted part of the system, and that a new axiom will show up in #print axioms for the theorem and for anything that depends on it. In versions of Lean up to 4.28, such theorems were marked instead by one shared axiom, Lean.trustCompiler.

That is a widening of what must be trusted, not a mistake in the answer. The prime is still prime. But a reader who wants to rely on the theorem must now trust a much larger body of code than the Lean kernel. The project this wiki records forbids native_decide in its own sources, as its proof gate states (see the transition page). Nothing is hidden either way: the axiom's name appears in the list, as on what has to be trusted.

What the calculation costs

Evaluation inside the logic is slow. It proceeds step by step through the definitions, with few of the shortcuts of a compiled program, and it has limits on how deep it may go. Asking the same question about 1009 shows the difference:

#eval isPrime 1009

example : isPrime 1009 = true := by decide

#eval prints true at once, but decide stops with maximum recursion depth has been reached. The option decide +kernel hands the evaluation directly to the Lean kernel, which evaluates the procedure once instead of twice:

theorem prime1009 : isPrime 1009 = true := by decide +kernel

#print axioms prime1009

This succeeds, and 'prime1009' does not depend on any axioms. The cost grows with the size of the question. In one measurement made for this page, on one computer, checking the same theorem for the six-digit prime 100003 with decide +kernel took about fifteen seconds, while running the program with #eval took well under a second. Other computers will give other times.

Some procedures cannot be evaluated inside the logic at all. A decision procedure defined by well-founded recursion may get stuck, because evaluating it would require working through proofs as well as data. The page on functions that always finish explains where such definitions come from.

The choice

Computing inside a proof is a trade between speed and trust. Evaluation by the Lean kernel is slow and bounded, but it adds nothing to what must be trusted. Evaluation by the compiler is fast, but it adds the compiler, and an axiom, to the foundation of the theorem. When a calculation is too large for the first, the alternatives include proving a general theorem that makes the calculation unnecessary, and accepting the larger trust and recording it. Lean makes the choice visible, so that a reader can see which was taken.

Next

• The small trusted core: what the Lean kernel is, and why it is kept small.
• Definitional equality: the technical treatment of computation in the logic.