1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29

import Mathlib

/-
# Pset 1

## 1.1

Visit https://adam.math.hhu.de/#/ and try one of the games! I recommend:

- Natural Number Game: The classic intro to Lean, although slightly tedious

- Set Theory Game: Another great intro to Lean with a focus on set theory

- Linear Algebra Game: I haven't played much of this one but it seems pretty good

- Real Analysis, The Game: Great except that some of the prose is currently AI slop, although the devs said they're going to rewrite all the slop

## 1.2

Follow these instructions for installing VS Code and Lean on your computer: https://lean-lang.org/install/

Next, clone the Git repo for this class and open the repo in VS Code: https://forgejo.mit.edu/xy/lean-iap

You might have to wait a few minutes for Lean to download Mathlib. Now open this file, and once the yellow loading bars on the left go away, put your cursor on the `#eval` line. If it says 6 in the InfoView on the right, then you're ready to Lean!
-/

open Nat

#eval 3!