wiki

Lean Proof Terms and Tactics

2 min read

Lean Proof Terms and Tactics

Context

Lean Theorem Prover exposes two complementary proof styles: direct proof terms and tactic scripts. Karunus2026 - All Lean Books And Where To Find Them highlights this distinction because many Lean learning paths move from seeing propositions as types, to writing proof terms, to using tactics that elaborate into kernel-checkable terms.

Formal Statement

In a propositions-as-types reading, a theorem statement is a type and a proof is a term inhabiting that type:

A tactic goal can be read as a proof judgment:

where Gamma is the local context and P is the target proposition. A tactic transforms one or more goals into subgoals, but the final result must elaborate to a proof term checked by Lean’s kernel.

For conjunction, a proof constructor has the schematic shape:

And.intro : P -> Q -> P /\ Q

Given h : P /\ Q, the term:

And.intro (And.right h) (And.left h)

constructs a proof of Q /\ P.

Derivation / Construction

Lean’s interactive workflow can be seen as search over proof terms. A tactic script manipulates the visible proof state, but it is not accepted merely because the tactic text ran; the elaborated term must type-check.

Definitions introduced by inductive declarations generate constructors and recursors. This is why induction, case analysis, and recursive definitions are central to Lean’s logic-facing and programming-facing sides. structure declarations package fields into records, and type-class arguments such as [Group G] ask instance search to fill in algebraic structure from the context.

Implications

  • Tactics are an interface to proof construction, not an alternative to proof checking.
  • Reading proof terms helps explain why tactics, recursors, and inductive definitions behave the way they do.
  • Lean metaprogramming extends this workflow by letting users write procedures that construct or transform proof terms programmatically.
  • The link to Intuitionistic Logic is through the proof-judgment and propositions-as-types view; imported classical axioms can add classical reasoning without changing the kernel requirement that proofs type-check.

Graph View

Backlinks