Lean for All

Day 7: Week 1 review: read it out loud🔗

Translate between Lean statements and plain English, both ways.

You can now read the language of statements. Here is everything from this week:

  • theorem name (variables) (hypotheses) : conclusion := proof

  • (n : Nat) or {n : Nat} or ∀ n : Nat, → “for every natural number n”

  • (h : P) before the colon, or P → after it → “if P, then”

  • ∧ and, ∨ or, ¬ not, ≠ not equal, ↔ if and only if

  • ∃ n, → “there is some n such that”

  • On Nat: 3 - 5 = 0, 7 / 2 = 3, 5 / 0 = 0

Reading a statement out loud in plain English is called informalizing it. It is the main skill of an auditor.

Try it on this one before you read the answer:

theorem mystery (a b : Nat) (h : a ≤ b) : ∃ c : Nat, a + c = b := ⟨b - a, a:Natb:Nath:a ≤ b⊢ a + (b - a) = b All goals completed! 🐙⟩

For all natural numbers a and b, if a ≤ b, then there is some c with a + c = b.

Notice the proof uses b - a as the witness, which is safe here because of the hypothesis a ≤ b (no stopping at zero). The Lab tab can produce a word-for-word English reading of any theorem: press Audit there. Today’s questions are a mix of everything.

Check yourself🔗