theorem

theorem は名前付きで命題を証明するためのコマンドです。より正確には、theorem は証明項を定義するためのコマンドだといえます。

/-- 自然数に右から0を足しても変わらない -/
theorem add_zero {n : Nat} : n + 0 = n := by simp

-- `add_zero` という項の型が、命題の内容になっている
#check (add_zero : ∀ {n : Nat}, n + 0 = n)

def との違い

theorem コマンドは特定の型を持つ項を定義するという意味で、def と同じです。実際、def を使っても証明項を定義することは可能です。しかし theorem を使っても関数などを定義することはできません。theorem で宣言できる項は命題のみです。

def add_zero' {n : Nat} : n + 0 = n := by simp

/--
error: type of theorem 'Theorem.frac' is not a proposition
  Nat → Nat
-/
theorem frac (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * frac n