Lean: Tactics

• Tactics: what a tactic proof builds
  2026-10-01 · Ryan Williams
  LeanLean: Tactics

  Part 3 of Lean from the Inside. A tactic proof looks like a list of instructions, which makes it feel like a different thing from a term. It isn't. The kernel only checks terms, and a by block is a program that builds one. This post looks at what that program builds, how it keeps track of the goals it has left, what the main automation tactics produce, and how to write a tactic of your own.