Numbers and Sets

• Course notes
• Example sheets
• Someone made an entire video series based on the course notes
  • Fields medalist supplementary reading and extra sheets

• Numbers, Sets and Axioms book by A.G. Hamilton

This is a free pdf from the library of US congress and teaches what the course wants us to know about deriving our own axioms and infinite sets.

• The Mechanics of Proof

This was written by a Cambridge Part III graduate using the Lean proof assistant. Covers 90% of the Cambridge course except infinite sets which the A.G. Hamilton book we'll do covers. We can use Lean to try and prove our own sample sheets and maybe exam answers too. To help us do that I will also do a short workshop on building our own proof assistant in Racket (Lisp/Scheme) to better understand how these proof assistants work.

• Algebra Via Problems free English (and Russian) copy on Arkadiy Skopenkov's website (and library genesis/anna's archive)

"I find that maths proofs are often 80% trivial algebra, and 10% magic tricks that are only relevant to that specific problem, and 10% key ideas that are used again and again." - Tripos graduate Neel Nanda

We're not doing every problem this is a math circle book where you find something interesting you don't know and fill in gaps.

Gitpod free tier as mentioned in the install instructions 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
  • 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 an annoying '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. 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 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 there could be 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 only looking at the signature not scrolling down to find the problem.

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

We're still doing the proofs by calc chapter.

1.4.1 example copy down some of the general rules

• Inequality preserved if C \(\ge\) 0:
• A \(\ge\) B implies CA \(\ge\) CB
• A \(\ge\) B implies A - C \(\ge\) B - C
• A \(\ge\) B and B > C then A > C

• Reversed inequality:
• A \(\ge\) B implies C - B \(\ge\) C - A
  • 2 \(\ge\) 1 implies 5 - 1 \(\ge\) 5 - 2

To get the full list of the unicode symbols every editor plugin comes with an abbreviations.json file. Place '\' (LaTeX style commands) before any of those symbols on the left of the abbreviations file to see them converted to the symbols on the right. For example \b is converted in the editor to \(\beta\)

\ge greater or equal
\le less than or equal
< and > are just keyboard chars

-- Example 1.4.2
-- Exercise: replace the words "sorry" with the correct Lean justification.
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 :=
  calc
    r = (s + r + r - s) / 2 := by ring
    _ ≤ (3 + (s + 3) - s) / 2 := by rel [h1, h2]
    _ = 3 := by ring

Example 1.4.3 think why is x + y <= x + (x + 5) it's because y <= x + 5 and x is <= to itself.

-- Example 1.4.3
-- Exercise: type out the whole proof printed in the text as a Lean proof.
example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 :=
  calc
  x + y ≤ x + (x + 5) := by rel [h1]
  _ = 2 * x + 5 := by ring 
  _ ≤ 2 * -2 + 5 := by rel [h2]
  _ < 2 := by numbers

Example 1.4.6 the final tactic is := by extra which is defined if you click on 'Index of Lean tactics' as "extra checks an inequality whose two sides differ by the addition of a positive quantity".

-- Example 1.4.9
-- Exercise: replace the words "sorry" with the correct Lean justification.
example {a b : ℚ} (h1 : a ≥ 0) (h2 : b ≥ 0) (h3 : a + b ≤ 8) :
    3 * a * b + a ≤ 7 * b + 72 :=
  calc
    3 * a * b + a
      ≤ 2 * b ^ 2 + a ^ 2 + (3 * a * b + a) := by extra
    _ = 2 * ((a + b) * b) + (a + b) * a + a := by ring
    _ ≤ 2 * (8 * b) + 8 * a + a := by rel [h3]
    _ = 7 * b + 9 * (a + b) := by ring
    _ ≤ 7 * b + 9 * 8 := by rel [h3]
    _ = 7 * b + 72 := by ring

1.4.10 same tactic used, put left hand side of inequality on right and side, add some positive squares. If you use any symbolic calculator online then the enormous expanded square makes sense as (a⁴ + b⁴ + c⁴)² = a⁸+2a⁴b⁴+2a⁴c⁴+b⁸+2b⁴c⁴+c⁸

Try some 14.11 exercises

example {a b : ℚ} (h1 : 3 ≤ a) (h2 : a + 2 * b ≥ 4) : a + b ≥ 3 :=
  calc
  a + b = a/2 + (a + 2*b)/2 := by ring
      _ ≥ 3/2 + 4/2 := by rel [h1,h2]
      _ ≥ 3 := by numbers

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  calc
  x ^ 3 - 8 * x ^ 2 + 2 * x = 
  x * x * x - 8 * x * x + 2 * x := by ring
  _ ≥ 9 * x * x - 8 * x * x + 2 * x := by rel [hx]
  _ = x * x + 2 * x := by ring
  _ ≥ 9 * x + 2 * x := by rel [hx]
  _ = 11 * x := by ring 
  _ ≥ 11 * 9 := by rel [hx]
  _ ≥ 3 := by numbers

example {n : ℤ} (hn : n ≥ 10) : n ^ 4 - 2 * n ^ 2 > 3 * n ^ 3 :=
  calc
  n^4 - 2 * n^2 =  
  n * n^3 - 2 * n^2 := by ring
  _ ≥ 10 * n^3 - 2 * n^2 := by rel [hn]
  _ = 3 * n^3 + 7 * n * n * n - 2 * n * n := by ring
  _ ≥ 3 * n^3 + 7 * 10 * n * n - 2 * n * n := by rel [hn]
  _ = 3 * n^3 + 68 * n * n := by ring
  _ ≥ 3 * n^3 + 68 * 10 * 10 := by rel [hn]
  _ > 3 * n^3 := by extra

Exercise 6 I couldn't figure it out in lean as I don't know enough of the standard library yet as there's no hypothesis to use rel or addarith with and the sig wants a rational number. My attempts using squares with the tactic extra failed too whereas by hand it is easy:

• x² - 2x \(\ge\) -1
• x² - 2x + 1 \(\ge\) -1 + 1
• (x - 1)² \(\ge\) 0
  • which we know is true since squares are always positive

Reading the second chapter.

2.1.2 prove m + 3 = 9 then final tactic is addarith to subtract 3 from both sides and show m = 9 - 3 or 6.

2.1.5 example remember extra checks an inequality whose two sides differ by the addition of a positive quantity and the square b² is always positive.

Another example is 2.1.7 of extra since positive quantities

example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
  have h3 : 0 ≤ b + a := by addarith [h1]
  have h4 : 0 ≤ b - a := by addarith [h2]
  calc
  a^2 ≤ a^2 + (b + a) * (b - a) := by extra
  _ = b^2 := by ring

2.1.8 extra tactic again:

example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
  have h2 : 0 ≤ b - a := by addarith [h]
  calc
  a^3 ≤ a^3 + ((b-a)*((b-a)^2 + 3*(b + a)^2)/4) := by extra
  _ = b^3 := by ring

The cancel tactic is defined as follows if you look at the code it's another tactic written for this book to simplify the regular lean libraries which are all abstract algebra we haven't learned yet.

'Cancel 2 at h' means

• 2x = 2y cancel to x = y
• 2x < 2y cancel to x < y
• x² = y² cancel to x = y
• 0 < 2x cancel to 0 < x
• x² = 0 cancel to x = 0

However in the exercises I couldn't get it work.

Example Ex 2.1.9 this is what I want to do but it won't let me despite x already being x > 1 so no possible way (x + 2) could be (-2 + 2) or 0:

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
  have h3 :=
  calc
  x * (x + 2) = 2 * (x ^ 2 + 2 * x)/2 := by ring
  _ = 2 * (4 + 2 * x)/2 := by rw [h1]
  _ = 2 * (x + 2) := by ring
  cancel (x + 2) at h3  

Another example from 2.1.9 that doesn't work, I tried after to manually add in (h : n > 0) and still fails:

example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by
  have hm : 0 = n ^ 2 - 4 * n + 4 := by addarith [hn]
  have h1 :=
  calc
  0 = n ^ 2 - 4 * n + 4 := by rw [hm]
  _ = (n - 2)^2 := by ring
  cancel 2 at h1 
  addarith [h1]

Others have had problems too and filed an issue for a possible bug or maybe I don't understand how Lean4 tactics work we'll have to skip these and try them again later when the author replies but reminder we are using a custom library for the purposes of learning and the regular Lean4 way of cancelling likely uses some fancy abstract algebra library we'll learn when we finish the groups course in Michaelmas.

TODO

---

Home