Lean4
Academy PassIntermediate18 lessons336 min

The Natural Number Lab

Build a complete elementary arithmetic theory in Lean. Define addition, develop multiplication and powers, construct an order relation, and finish with divisibility arguments. The reference proofs use explicit inductions, witnesses and multi-step calc chains rather than hiding the mathematics in one-line automation.

Sign in to track your progress
Start the course
  1. Addition world5 lessons
  2. Addition from recursionStart from zero and successor, then prove the first identity by induction.15 min
  3. Move a successor across additionProve the equation the recursive definition does not compute for you.16 min
  4. Addition commutesCombine the first two lemmas in a structured induction.18 min
  5. Addition associatesControl three nested unfolds and expose the induction hypothesis.18 min
  6. Cancel a common tailRewrite inside a hypothesis and recover equality of the starting values.20 min
  7. Multiplication world5 lessons
  8. Zero times everythingRebuild the left-zero law directly from multiplication recursion.14 min
  9. Move a successor through multiplicationExpose recursive products, then finish the visible arithmetic.18 min
  10. Multiplication distributesProve distributivity one successor at a time without a broad simplifier.20 min
  11. Multiplication commutesPair left and right recursion laws in the induction step.18 min
  12. Multiplication associatesUse distributivity as a local step inside a larger induction.22 min
  13. Power world2 lessons
  14. Adding exponentsProve that exponent addition becomes multiplication of powers.20 min
  15. Powers of a productInduct, then commute the middle factors with a controlled normalization.22 min
  16. Order world3 lessons
  17. Order as a gapDefine an order relation with an existential witness and prove reflexivity.14 min
  18. Compose two gapsBuild a transitivity witness and document the route with calc.20 min
  19. Two directions force equalityExpose hidden gaps and derive antisymmetry from their equations.18 min
  20. Divisibility world3 lessons
  21. Compose divisibility witnessesMultiply two quotient witnesses and associate the resulting product.20 min
  22. A divisor of a sumAdd quotient witnesses and factor the common divisor.18 min
  23. Finale: chain, add and factorSynthesize three hypotheses in a long, readable divisibility proof.25 min