1. Foundations in Lean
3. Basics
4. 1. Overview of Lean
6. Type Theory
7. 2. λ-Calculus
8. 3. Propositional Logic
9. 4. Curry-Howard Isomorphism
10. 5. Inductive Types
12. Logic
13. 6. Propositional Connectives
14. 7. First Order Logic
15. 8. Tactics
16. 9. Equality
17. 10. Sets and Relations
19. Basic Numbers
20. 11. Natural Numbers
21. 1. 11.1. Definition
    2. 11.2. Properties
22. 12. Integers
23. 1. 12.1. Quotient Spaces
    2. 12.2. Operators
    3. 12.3. Properties
24. 13. Rational Numbers
26. Real Numbers
27. 14. Overview
28. 15. Dedekind Cuts
29. 16. Addition
30. 17. Subtraction
31. 18. Maximum
32. 19. Multiplication
34. Partial Orders
35. 20. Definitions
36. 21. Properties
37. 22. Maps
38. 23. Strings
39. 24. Information
40. 25. The D.M. Completion
42. Appendix
43. 26. Helpers