Natural Numbers

The natural numbers are where mathematics begins. Zero, successor, induction — from these three ideas, all of arithmetic follows. In Lean 4, natural numbers are defined inductively: there is zero, and for every natural number there is a successor.

  1. 01 Zero and successor easy
  2. 02 Addition is associative easy
  3. 03 Addition is commutative medium
  4. 04 Induction medium
  5. 05 Multiplication distributes over addition hard
← All tracks Start →