Home / Tracks / Logic / True is true

True is true

The mathematics

True is the simplest proposition in all of logic. It's always true. There's nothing to debate, nothing to assume, nothing to unpack. It just is.

In everyday reasoning, "True" is so obvious you'd never bother stating it. But in formal logic, we need a way to represent the concept of something that is unconditionally true. That's what True does.

In Lean 4, True is a type (a proposition) that has exactly one constructor: True.intro. Think of it as a certificate that says "yes, this is true" — and there's always exactly one such certificate available. Because there's always a proof of True, it's the easiest theorem you'll ever prove.

The Lean 4 proof

Lean provides a tactic called trivial that handles goals which are, well, trivial. The goal True is the classic example. You can also write exact True.intro to supply the proof term directly.

-- Using the trivial tactic
theorem true_is_true : True := by
  trivial

-- Using the proof term directly
theorem true_is_true' : True := by
  exact True.intro

-- You don't even need tactics — a term-mode proof works too
theorem true_is_true'' : True := True.intro

All three are valid. The trivial tactic is the most idiomatic for simple goals like this.

Your turn

Replace sorry with a proof. Copy this into Lean 4 Web and make it compile.

theorem my_first_proof : True := by
  sorry

theorem my_first_proof : True := by
  trivial