How Mathematicians can Get Started with Lean

Instructions from the video: Step 1: Open a free account on https://github.com/ Step 2: Google "Mathlib4" or navigate to https://github.com/leanprover-community/mathlib4 Step 3: Scroll down to the "Open in GitHub Codespaces" button (or just click here: https://codespaces.new/leanprover-community/mathlib4) Step 4: Wait 5ish minutes for Lean to load (just for the first time you open codespaces). Step 5: Make a new file somewhere called "something.lean", type "import Mathlib" on the first line, wait a few moments for it to load, and start playing!