PMA Publisher: Published from the Principia Machina source

2026-10-15T19:34:34Z

Published from the Principia Machina source

← Older revision		Revision as of 19:34, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Automation and its limits}}		{{DISPLAYTITLE:Automation and its limits}}
	{{Technical\|Lean theorem prover/System/Decision procedures}}		{{Technical\|Lean theorem prover/System/Decision procedures}}
			{{Lean theorem prover map}}

	Some tactics do not wait to be told each step. Given a goal, they search for a proof		Some tactics do not wait to be told each step. Given a goal, they search for a proof

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:00:52Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Automation and its limits}}
{{Technical|Lean theorem prover/System/Decision procedures}}

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 ==

<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 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
</pre>

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.<ref name="ref-simp">''The Lean Language Reference'', version for Lean 4.34.0
(lean-lang.org, 2026), chapter 15, "The Simplifier".
https://lean-lang.org/doc/reference/4.34.0/The-Simplifier/</ref> 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.<ref name="ref-tacref">''The Lean
Language Reference'', version for Lean 4.34.0 (lean-lang.org, 2026), section 14.5, "Tactic
Reference": entries for <code>omega</code> and <code>decide</code>.
https://lean-lang.org/doc/reference/4.34.0/Tactic-Proofs/Tactic-Reference/</ref> 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.<ref name="ref-tacref" /> 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;
[[Lean theorem prover/Explainers/Computation inside proofs|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.<ref name="ref-grind">''The Lean Language
Reference'', version for Lean 4.34.0 (lean-lang.org, 2026), chapter 16, "The grind tactic".
https://lean-lang.org/doc/reference/4.34.0/The--grind--tactic/</ref>

== When the search fails ==

<pre class="lean lean-fails" 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;">
example (x y : Nat) (h : x * y = 6) : y ≤ 6 := by omega
</pre>

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 <code>omega could not
prove the goal:</code> and offers "a possible counterexample" in which <code>y</code> 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.<ref name="godel">Kurt Gödel, "Über formal
unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", ''Monatshefte für
Mathematik und Physik'' 38 (1931), pp. 173–198. doi:10.1007/BF01700692</ref><ref name="raatikainen">Panu
Raatikainen, "Gödel's Incompleteness Theorems", ''The Stanford Encyclopedia of Philosophy''
(first published 2013, substantive revision 8 October 2025), sections 1 and 4.2.
https://plato.stanford.edu/entries/goedel-incompleteness/</ref>

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.<ref name="church">Alonzo Church, "A note on the
Entscheidungsproblem", ''Journal of Symbolic Logic'' 1 (1936), pp. 40–41.
doi:10.2307/2269326</ref><ref name="turing">A. M. Turing, "On Computable Numbers, with an
Application to the Entscheidungsproblem", ''Proceedings of the London Mathematical Society'',
series 2, vol. 42 (1936–37), pp. 230–265. doi:10.1112/plms/s2-42.1.230</ref><ref name="copeland">B.
Jack Copeland, "The Church-Turing Thesis", ''The Stanford Encyclopedia of Philosophy'' (first
published 1997, substantive revision 18 December 2023), section 1.7.
https://plato.stanford.edu/entries/church-turing/</ref> 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.<ref name="raatikainen" /> Robinson arithmetic has seven axioms, simple facts about
zero, the next number, addition and multiplication.<ref name="raatikainen" /> 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
<code>Nat.succ x</code> is the number after x and the last four hold by calculation:

<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;">
-- 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
</pre>

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.<ref name="raatikainen" /> In practice the limit means that some procedures in Lean
work within a class of statements chosen so that a method exists, as <code>decide</code>
does for finite checks, while others, such as <code>simp</code> and <code>grind</code>, 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 <code>grind</code> that it
produces ordinary proof terms for every fact it adds.<ref name="ref-grind" /> A bug in
automation can therefore cost time or produce a confusing message; it cannot make Lean accept
a false theorem.<ref name="ref-tactics">''The Lean Language Reference'', version for Lean
4.34.0 (lean-lang.org, 2026), chapter 14, "Tactic Proofs".
https://lean-lang.org/doc/reference/4.34.0/Tactic-Proofs/</ref> Keeping the search for a
proof apart from its checking is an established technique in the LCF tradition from which tactics
come.<ref name="gordon">Michael J. C. Gordon, "From LCF to HOL: a short history", in Gordon
Plotkin, Colin Stirling and Mads Tofte (eds), ''Proof, Language, and Interaction: Essays in
Honour of Robin Milner'', MIT Press, 2000.
https://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html</ref>

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

== Next ==

* [[Lean theorem prover/Explainers/When Lean says no|When Lean says no]]: reading the messages of a failed check.
* [[Lean theorem prover/System/Decision procedures|Decision procedures]]: the technical treatment.

== References ==

<references />

Lean theorem prover/Explainers/Automation and its limits - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source