Automation and its limits

Technical version: 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 tactics do not wait to be told each step. Given a goal, they search for a proof themselves. This page describes four such tactics, says what each one searches, explains why no procedure can settle every question, and shows why a proof found by search is checked like any other.

Four searching tactics

theorem by_simp (xs : List Nat) : (xs ++ []).length = xs.length := by simp

theorem by_omega (x y : Nat) (h1 : x + 2 * y = 10) (h2 : 3 ≤ y) : x ≤ 4 := by omega

theorem by_decide : ∀ n : Fin 8, n.val * n.val % 8 ≠ 2 := by decide

theorem by_grind (f : Nat → Nat) (a b : Nat) (h1 : a = b) (h2 : f a = 3) :
    f b = 3 := by grind

#print axioms by_simp
#print axioms by_omega
#print axioms by_decide
#print axioms by_grind

Each theorem is proved by a single word, and Lean accepts all four.

simp, the simplifier, rewrites the goal with a large stock of equations marked as simplification rules, working from the inside of an expression outwards, until no rule applies. Here it knows that appending the empty list changes nothing, and the two sides become the same. It searches for places where a known equation applies. It cannot prove what does not follow by such rewriting.

omega settles problems of linear arithmetic over whole numbers: equations and inequalities built from unknowns, addition, and multiplication by fixed numbers, with division and remainder by fixed numbers. The reference manual calls it not yet a full decision procedure, but effective on many problems. In the example, x + 2y = 10 and y of at least 3 force x to be at most 4.

decide computes. It finds a procedure that decides the statement, runs it, and if the answer is "true", the run is the proof. The example checks the eight numbers from 0 to 7 and finds that none has a square leaving remainder 2 on division by 8. It works only when the statement contains no unknowns and a deciding procedure is available; computation inside proofs says more.

grind gathers facts and works on them with several methods at once. The reference manual pictures a shared whiteboard: each new equation or inequality is written on it, terms known to be equal are grouped together, and each method reads from the board and adds to it. The methods include merging equals (if a = b, then f a = f b), using known theorems that fit, splitting into cases, and solvers for linear arithmetic over the integers and for algebra. It always argues by contradiction: it assumes the goal is false and looks for an impossibility. It is not designed for problems whose cases multiply out of control, such as large instances of the pigeonhole principle.

When the search fails

example (x y : Nat) (h : x * y = 6) : y ≤ 6 := by omega

The statement is true: if x times y is 6, then y divides 6, so y is at most 6. But a product of two unknowns lies outside linear arithmetic. Lean 4.34.1 answers omega could not prove the goal: and offers "a possible counterexample" in which y is at least 7. The counterexample is only possible. It solves the simplified problem that omega could see, in which the product says nothing about y, not the real one. A failed search is information, not a verdict: the statement may still be true, and this procedure cannot see why.

Why no procedure does everything

Two results from the 1930s mark the limit, and they are different results.

The first concerns what can be proved at all. Kurt Gödel showed in 1931, in a form that J. Barkley Rosser strengthened in 1936, that any consistent formal system in which a certain amount of elementary arithmetic can be carried out contains statements that it can neither prove nor disprove.

The second concerns what a machine can decide. Alonzo Church and Alan Turing showed independently in 1936 that there is no mechanical method which decides, for every formula of first-order logic, whether it can be proved. The same holds for every consistent system that contains, or can interpret, a weak theory of arithmetic called Robinson arithmetic: there is no mechanical way to tell its theorems from its other statements. Robinson arithmetic has seven axioms, simple facts about zero, the next number, addition and multiplication. Every statement of arithmetic can be read as a Lean statement about Lean's natural numbers, and read that way all seven axioms are theorems of Lean; the block below proves each in one line, where Nat.succ x is the number after x and the last four hold by calculation:

-- 1. Zero is not the number after any number.
theorem q1 (x : Nat) : Nat.succ x ≠ 0 := Nat.succ_ne_zero x
-- 2. Different numbers have different numbers after them.
theorem q2 (x y : Nat) (h : Nat.succ x = Nat.succ y) : x = y := Nat.succ.inj h
-- 3. Every number other than zero is the number after some number.
theorem q3 (x : Nat) (h : x ≠ 0) : ∃ y, x = Nat.succ y := Nat.exists_eq_succ_of_ne_zero h
-- 4 to 7. Addition and multiplication, by recursion on the second number.
theorem q4 (x : Nat) : x + 0 = x := rfl
theorem q5 (x y : Nat) : x + Nat.succ y = Nat.succ (x + y) := rfl
theorem q6 (x : Nat) : x * 0 = 0 := rfl
theorem q7 (x y : Nat) : x * Nat.succ y = x * y + x := rfl

Lean 4.34.1 accepts all seven. A procedure that decided provability in Lean would therefore also decide which statements of arithmetic Lean proves. Those statements form a system that contains Robinson arithmetic and is consistent if Lean's logic is, so the result just stated rules such a procedure out. If Lean's logic is consistent, then, no tactic, however clever, can decide for every statement whether Lean can prove it.

The word "undecidable" is used for both results, in two senses: a single statement that a system can neither prove nor disprove, and a whole class of questions that no machine can answer. In practice the limit means that some procedures in Lean work within a class of statements chosen so that a method exists, as decide does for finite checks, while others, such as simp and grind, are searches that often succeed and sometimes give up. Beyond them, a person still has to find the idea.

Found by search, checked by the Lean kernel

However a tactic finds its proof, what it hands over is an ordinary proof term, and the Lean kernel checks that term like any other. The manual says of grind that it produces ordinary proof terms for every fact it adds. A bug in automation can therefore cost time or produce a confusing message; it cannot make Lean accept a false theorem. Keeping the search for a proof apart from its checking is an established technique in the LCF tradition from which tactics come.

The #print axioms lines above show what the four proofs rest on. Lean 4.34.1 answers that by_decide does not depend on any axioms, that by_simp depends on propext, that by_omega depends on propext and Quot.sound, and that by_grind depends on those two and Classical.choice. These are Lean's three standard axioms, described in what the axioms are. Nothing was added by the search.

Next

• When Lean says no: reading the messages of a failed check.
• Decision procedures: the technical treatment.