Proving · 10 min

Mathematical symbols

Lean uses Unicode characters directly in source code. Type a backslash abbreviation, such as \forall, and accept the editor suggestion with Enter or Tab. You can also paste the symbol. Greek letters such as α and β are ordinary identifiers, often used for types.

Read ∀ n : Nat, ∃ m : Nat, n < m as “for every natural number n, there is a natural number m greater than n.” The witness m can depend on n. To prove it, introduce n and supply n + 1 together with a proof of the inequality.

P ∧ Q means both P and Q; P ∨ Q means at least one; ¬P means P implies False. P → Q is implication, while A → B is a function type for data. P ↔ Q requires proofs in both directions. In an error message, ⊢ marks the goal below the available assumptions.

Symbols can have different meanings in different contexts. ← extracts an action’s result in a do block, but reverses an equality in rw [← h]. ⟨…⟩ constructs a value based on its expected type. A leading · focuses a proof goal, while (· + 1) creates an anonymous function.

Exercise

Prove that every natural number has a larger natural number.

theorem larger : ∀ n : Nat, ∃ m : Nat, n < m := by
  sorry

theorem larger : ∀ n : Nat, ∃ m : Nat, n < m := by
  intro n
  exact ⟨n + 1, by omega⟩

Related example