Tactic Mode vs Term Mode in Lean 4

Why This Matters

In Lean 4, the same theorem can be proved by writing the proof term directly or by invoking tactics inside a by ... block. The kernel sees the same term either way. The choice is about the human writing and reading the proof: and the two modes have different ergonomic profiles.

A short, structural proof reads naturally as a term. A proof with case analysis, rewriting, or extended computation reads more clearly as a sequence of tactics. Mathlib4 follows a consistent convention: definitions and very short proofs use term mode; theorems with body more than a few lines use tactic mode. This page gives the operational rule and shows the two modes on the same examples.

The Same Theorem in Both Modes

The theorem "for all natural numbers $n$, $n + 0 = n$":

Term mode:

theorem add_zero (n : Nat) : n + 0 = n :=
  rfl

Tactic mode:

theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

The by keyword opens tactic mode. Everything until the end of the proof is a tactic block. The block produces a term; the kernel checks that term against the declared type. In this case both proofs elaborate to identical terms.

A multi-step example: "for $a \leq b$ and $c \leq d$, $a + c \leq b + d$".

Term mode:

theorem add_le_add {a b c d : Nat} (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d :=
  Nat.add_le_add h1 h2

(Mathlib provides the lemma; term mode applies it directly.)

Tactic mode:

theorem add_le_add {a b c d : Nat} (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
  exact Nat.add_le_add h1 h2

The exact tactic accepts a complete proof term. This is the way tactic mode wraps a term-mode proof.

Both elaborations produce identical kernel terms. The difference is the writing experience: term mode reads as one expression; tactic mode reads as one tactic ("exact this") with the term embedded.

When Term Mode Wins

Term mode is shorter and more direct for:

Definitional rewrites that close in one step. rfl, Eq.refl, Nat.zero_le _, or a direct lemma application.

Constructions where the proof is the data. A function from Nat to Nat is also a definition; an inhabitant of ∃ x, P x is a pair. Writing ⟨3, by norm_num⟩ to provide both the witness and the proof keeps the structure visible. Hiding the witness behind a tactic would obscure it.

Single-step intro then apply. If your tactic-mode proof is intro h; apply lemma; exact h, term mode is shorter: fun h => lemma h.

Pure definitions. When the theorem is a definition packaged as a function (e.g., a structure projection or a derived instance), term mode is natural and tactic mode would be performative.

Heuristic: if the proof fits comfortably on one line, prefer term mode.

When Tactic Mode Wins

Tactic mode is shorter and clearer for:

Case analysis. Goals with multiple subgoals after induction or cases are best handled by tactics; the alternative is nested match expressions in term mode that are hard to read.

Equational rewriting. rw [lemma1, lemma2, lemma3] is much cleaner than the explicit term lemma3.symm.trans (lemma2.symm.trans (lemma1.symm.trans rfl)).

Closing goals by automation. simp, omega, aesop, decide, norm_num, polyrith, positivity are all tactics. They are routinely the fastest way to close arithmetic, linear-algebra, and inequality goals.

Proofs that explore the goal. When you do not yet know the final shape of the proof, tactic mode lets you build it incrementally with the goal view updating after each step. Term mode requires the entire proof up front.

Heuristic: if the proof has more than one step of substantive work, prefer tactic mode.

Operational Rule

The community convention in Mathlib4:

• Proofs of one expression: term mode, := rfl or := Lemma.foo.
• Proofs of two or more substantive steps: tactic mode, := by ....
• Definitions and structure instances: term mode, even when the body is long.
• Side conditions on local hypotheses introduced via have: term mode if one line, have ... := by ... if the side condition needs tactics.

Mathlib4 style enforces this with linting that flags single-tactic by exact ... blocks as redundant; they should be unwrapped to term mode.

Mixing the Two

The two modes interleave freely. A typical pattern:

theorem something (n : Nat) (h : n ≠ 0) : n + 1 ≥ 2 := by
  -- tactic mode
  have h1 : n ≥ 1 := Nat.one_le_iff_ne_zero.mpr h  -- term-mode have
  -- back in tactic mode
  omega

The have step is term-mode (the right-hand side after := is an expression). The surrounding proof is tactic-mode. This is idiomatic: short term-mode steps inside a tactic-mode skeleton.

The reverse is also possible: by blocks can appear inside term-mode expressions. To provide an existential witness with a tactic-mode proof:

example : ∃ n : Nat, n > 5 :=
  ⟨6, by omega⟩

The angle brackets are term-mode (pair constructor); the right component uses tactics to discharge the side condition.

Common Misconceptions

Worked Example: Three Modes, One Proof

Prove: "if $n$ is odd, then $n^2$ is odd," where odd is defined as ∃ k, n = 2 * k + 1.

Term mode:

theorem odd_sq {n : Int} (h : ∃ k, n = 2 * k + 1) : ∃ m, n^2 = 2 * m + 1 := by
  rcases h with ⟨k, rfl⟩
  refine ⟨2 * k^2 + 2 * k, ?_⟩
  ring

(Here we use a tactic-mode skeleton because the result needs the witness $m = 2k^2 + 2k$ and a ring rewrite. A pure-term version would need to spell out the entire algebraic identity, which is unreadable.)

Pure tactic mode:

theorem odd_sq {n : Int} (h : ∃ k, n = 2 * k + 1) : ∃ m, n^2 = 2 * m + 1 := by
  obtain ⟨k, rfl⟩ := h
  use 2 * k^2 + 2 * k
  ring

Pure term mode (anti-pattern, shown for contrast):

theorem odd_sq {n : Int} (h : ∃ k, n = 2 * k + 1) : ∃ m, n^2 = 2 * m + 1 :=
  Exists.elim h (fun k hk =>
    ⟨2 * k^2 + 2 * k, by subst hk; ring⟩)

The third version still calls ring inside a by block: pure term mode is impractical here because ring is the right closing tactic for polynomial identities.

The first two are equivalent and both idiomatic Mathlib4. The third is what you avoid: the destructuring is harder to read in Exists.elim than in obtain.

Exercise

Problem. Prove in Lean 4 that for natural numbers $a$ and $b$, $(a + b)^2 = a^2 + 2 a b + b^2$. Provide both a one-line term-mode proof and a tactic-mode proof. Which is shorter?

Hint. ring is in Mathlib.

Solution.

Term mode:

example (a b : Nat) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by ring

Tactic mode (same thing, just explicit):

example (a b : Nat) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by
  ring

Both proofs are one line. The tactic-mode version is one newline longer but they read identically. For a polynomial identity, ring is the close, and tactic mode is conventional. The "pure term mode" version would expand (a + b)^2 manually using Nat.add_mul, Nat.mul_add, Nat.add_assoc, and Nat.add_comm: pages of term construction for what tactic mode handles in a single token.

Implementation Note

VS Code's Lean 4 extension shows the current goals in the right panel. In tactic mode, the panel updates after every tactic; you can see the goal evolve. In term mode, the goal is only displayed where the elaborator pauses (typically at a _ placeholder or at the top of the term).

A common workflow: start with := by sorry, run the file, and read the goal in the panel. Then write tactics one at a time, watching the goal shrink. When the goal is closed, the proof is done. Convert to term mode at the end only if the final proof is one line.

The Mathlib4 style preference: tactic mode by default for non-trivial proofs, term mode for the one-liners. The convention reduces refactoring friction.

Connection to TheoremPath

Most theorems in the FormalSLT manifest use tactic mode because they involve case analysis, rewriting with named lemmas, or invocations of decision procedures. The Hoeffding finite-sum proof, for example, is roughly 200 lines of tactics. A term-mode equivalent would be unreadable. The worked Lean proof tour walks through that file annotated.

See /methodology for the rationale on why FormalSLT proofs are kernel-checked rather than human-checked, and /evidence for the audit trail per theorem.