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!