A 2024 Computer Science Curriculum

The categories course has recorded lectures but the lecture notes are high enough quality they can be used as a workbook. You don't have to do everything here obviously take only what you want.

Gitpod free tier is easiest. To install Lean locally w/Visual Studio:

• install Lean
• install git
• install code (Visual Studio code) though I use emacs see below
• in terminal type: git clone https://github.com/hrmacbeth/math2001.git
• cd math2001
• in terminal: lake exe cache get
  • it downloads 3972+ files (wtf)
• 'code .' to start from present directory
• install lean4 extension

Click on 01ProofsbyCalculation.lean you should get a right panel opening up in VS code called 'Lean Infoview' that displays tactic state goals and all messages.

Install everything as before then git clone lean4-mode, paste the readme elisp into .emacs or init.el file, restart and open any .lean file. Ctrl-c Ctrl-i opens the lean view in a new window showing goals. If you use vanilla emacs from some distros like Ubuntu you'll have some 'can't verify signature' error which is fixed by updating elpa keyring.

Another way is with gpg:

gpg --homedir ~/.emacs.d/elpa/gnupg --list-keys 

/home/x/.emacs.d/elpa/gnupg/pubring.kbx
-----------------------------------------
pub   dsa2048 2014-09-24 [SC] [expired: 2019-09-23]
      CA442C00F91774F17F59D9B0474F05837FBDEF9B
uid           [ expired] GNU ELPA Signing Agent (2014) <elpasign@elpa.gnu.org>

pub   rsa3072 2019-04-23 [SC] [expires: 2024-04-21]
      C433554766D3DDC64221BFAA066DAFCB81E42C40
uid           [ unknown] GNU ELPA Signing Agent (2019) <elpasign@elpa.gnu.org>

pub   ed25519 2022-12-28 [C] [expires: 2032-12-25]
      AC49B8A5FDED6931F40EE78BF993C03786DE7ECA
uid           [ unknown] GNU ELPA Signing Agent (2023) <elpasign@elpa.gnu.org>
sub   ed25519 2022-12-28 [S] [expires: 2027-12-27]

Update key if your second key is expired:

gpg --homedir ~/.emacs.d/elpa/gnupg --keyserver hkps://keys.openpgp.org --recv-keys 066DAFCB81E42C40

Reading 1.1 Proving equalities from Mechanics of Proof. Any examples you don't understand come back here after writing some Lean proofs you won't get them all immediately. First example expand out (a - b) and notice you need to add 4ab in order to balance both sides. The problem statement tells us (a - b) = 4 so (a - b)² is 16 after substitution.

1.2.x Proving equalities in Lean the .lean files are all included in the Math2001 directory you cloned from github. I had to fight with Lean to get it to accept 1.2.4 so rewrote it exactly like she did with parens:

-- Example 1.2.4.
-- Exercise: type out the whole proof printed in the text as a Lean proof.
example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) :
    d * (a * f - b * e) = 0 := 
   calc
    d * (a * f - b * e)
      = d * a * f - d * b * e := by ring
    _ = (a * d) * f - d * b * e := by ring
    _ = (b * c) * f - d * b * e := by rw [h1]
    _ = b * (c * f) - d * b * e := by ring
    _ = b * (d * e) - d * b * e := by rw [h2]
    _ = 0 := by ring 

We are using 'calc' in Lean hence the name proof by calculation. I'm guessing the underscore represents the entire left hand side of the equation indicating to the rw (rewrite) pattern matcher to ignore it. There's nothing in the documentation I could easily find but Terence Tao describes the underscore here same way.

Look at the infoview/goals it will tell you when that stage is done by 'goals accomplished', also click around various parts of the proof to see how the infoview changes:

-- Example 1.3.2
example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  calc
  x = (x + 4) - 4 := by ring
  _ = 2 - 4 := by rw [h1]
  _ = -2 := by ring 

I guessed the syntax for rationals in Lean and it worked:

-- Example 1.3.4
example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 :=
  calc
  w = (3 * w + 1)/3 - 1/3 := by ring
  _ = 4/3 - 1/3 := by rw [h1]
  _ = 1 := by ring

1.3.11 you can use Lean to tell you when the sides have been balanced. You did it correctly if goals panel or infoview shows goals accomplished and the linter hasn't added any red squiggle lines or other errors. Some exercises I tried, you can rewrite a line using both hypotheses and eliminate a lot of steps I kept them here for illustration how Lean works:

example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 :=
  calc
  u = (4 * u + v)/4 - v/4 := by ring
  _ = 3/4 - 2/4 := by rw [h1, h2]
  _ = 1/4 := by ring

example {u v : ℝ} (h1 : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
  calc
  u ^ 2 + 3 * u + 1 = (u + 1) * (u + 1) + (u + 1) - 1 := by ring
  _ = v * v + v - 1 := by rw [h1]
  _ = v ^ 2 + v - 1 := by ring

1.3.2 once again we first establish x = x then use the hypothesis to rewrite it

-- Example 1.3.2
example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  calc
  x = (x + 4) - 4 := by ring
  _ = 2 - 4 := by rw [h1]
  _ = -2 := by ring

For the rest of these examples try them yourself going through the 03TipsandTricks.lean file before looking at the solution it's the only way you learn.

-- Example 1.3.5
example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 :=
  calc
  x = (2 * x) - x  := by ring
  _ = 2 * x - (2 * x + 3) := by rw [h1]
  _ = -3 := by ring

(╯°□°)╯︵ ┻━┻ if you see calc underlined with a red error it means you forgot an equal sign or _ sign in your chain of rewrites or there is an accidental character floating around in the scope out of view somewhere it took me forever to figure that out as Lean kept giving some cryptic message and I was looking at the signature.

1.3.11 exercises all use the examples we just saw. Look at 1.3.8 example when you try exercise 11 and manipulate it so a = (4 + 2) / 3.

example {x y : ℝ} (h1 : x = 3) (h2 : y = 4 * x - 3) : y = 9 :=
  calc
  y = y := by ring
  _ = 4*x - 3 := by rw [h2]
  _ = 4*3 - 3 := by rw [h1]
  _ = 9 := by ring

example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 :=
  calc
  p = (5*p -3 - 3*p + 1)/2 + 1 := by ring
  _ = (3*p + 1 - 3*p + 1)/2 + 1 := by rw [h1]
  _ = 2/2 + 1 := by ring
  _ = 2 := by ring

TODO