Numbers and Sets

• Course notes (unofficial)
  • Someone made an entire video series based on the course notes
• Example sheets
• Final exams

Look at some of the old exams without looking at the recent exams because you want to test yourself and have no advantage that way you'll know if your strategy is working to actually learn the tripos yourself. Every current Cambridge student would have access to these old exams anyway.

The sheets:

• First sheet is almost entirely number theory (primes).
• Second is divisibility, mod, RSA encryption, more number theory.
• Third is converging sequences, least upper bound axiom, proving something to be irrational. - Fourth is sets (countable) and functions.

Many of these example sheet problems are almost identical to the Algebra via Problems content.

Now that we've looked through the sheets and old exams we can create our own curriculum since we don't have access to Cambridge lectures

• Intro to Number Theory lectures by Richard Borcherds
  • First 26 lectures all showed up in old exams/sheets
• The Mechanics of Proof written by a Cambridge Part III graduate using the Lean proof assistant.

Some optional practice:

• Algebra Via Problems free English (and Russian) copy on Arkadiy Skopenkov's website (and library genesis/anna's archive)
• Supplementary reading and extra sheets about countability

There is content about convergence (limits/calculus) that I moved to the differential equations page since we have to learn calculus there anyway.

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
• 'code .' to start from present directory
• install lean4 extension

Open any .lean extension file and you should get a right panel opening up in VS code called 'Lean Infoview' that displays tactic state goals as you click around the source code.

Install lean4-mode and Ctrl-c Ctrl-i opens the lean view in a new window showing goals.

Reading 1.1 Proving equalities from Mechanics of Proof. The goal here is to make both sides equal, with the right side finessed using algebra so it can be rewritten by a hypothesis such as a - b = 4 in the first example.

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 

The underscore tells the matcher to ignore the left hand side of the equation when rewriting or other actions as we are presently working only with the right hand side. Look at the infoview/goals it will tell you when that stage is done by 'goals accomplished'. Try clicking 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 

You can rewrite a line using both hypotheses and eliminate some steps:

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

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 renegade character I mistyped.

1.3.11 exercises all use the examples we just saw except the last 2:

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

example {a b : ℤ} (h : a - b = 0) : a = b :=
  calc
  a = a - 0 := by ring
  _ = a - (a - b) := by rw [h]
  _ = b := by ring

example {x y : ℤ} (h1 : x - 3 * y = 5) (h2 : y = 3) : x = 14 :=
  calc
  x = x - (3 * y) + (3 * y) := by ring
  _ = 5 + (3 * 3) := by rw [h1, h2]
  _ = 14 := by ring

example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  calc
  p = p - (2 * q) + (2 * q) := by ring
  _ = 1 + (2 * -1) := by rw [h1, h2]
  _ = -1 := by ring

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

example {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 :=
  calc
  p = p + 4 * q - 4 * (q - 1) - 4 := by ring
  _ = 1 - 4 * 2 - 4 := by rw [h1, h2]
  _ = -11 := by ring

example {a b c : ℝ} (h1 : a + 2 * b + 3 * c = 7) (h2 : b + 2 * c = 3)
  (h3 : c = 1) : a = 2 :=
  calc
  a = (a + 2 * b + 3 * c) - 2 * (b + 2 * c) + c  := by ring
  _ = 7 - 2 * 3 + 1 := by rw [h1, h2, h3]
  _ = 2 := by ring

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 {c : ℚ} (h1 : 4 * c + 1 = 3 * c - 2) : c = -3 :=
  calc
  c =  4 * c + 1 - 3 * c - 1 := by ring
  _ = 3 * c - 2 - 3 * c - 1 := by rw [h1]
  _ = -3 := 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

example {x y : ℤ} (h1 : 2 * x + y = 4) (h2 : x + y = 1) : x = 3 :=
  calc
  x = 2 * x + y - 1 * (x + y) := by ring
  _ = 4 - 1 * 1 := by rw [h1, h2]
  _ = 3 := by ring

example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 :=
  calc
  a = (a + 2 * b + 2 * (a - b)) / 3 := by ring
  _ = (4 + 2 * 1)/3 := by rw [h1, h2] 
  _ = 6/3 := by ring
  _ = 2 := 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)^2 + u + 1 - 1 := by ring
  _ = v^2 + u + 1 - 1 := by rw [h1]
  _ = v^2 + v - 1 := by rw [h1]
 -- red squiggle on last rw...??
 -- this should work but I gave up

 -- use symbolab.com or similar site to divide 
 -- this is directly from one of the examples in the book
example {t : ℚ} (ht : t ^ 2 - 4 = 0) :
    t ^ 4 + 3 * t ^ 3 - 3 * t ^ 2 - 2 * t - 2 = 10 * t + 2 :=
    calc
    t^4 + 3* t^3 - 3* t^2 - 2 * t - 2 =
    (t^2 + 3 * t + 1) * (t^2 - 4) + 10 * t + 2 := by ring
    _ = (t^2 + 3 * t + 1) * 0 + 10 * t + 2 := by rw [ht]
    _ = 10 * t + 2 := by ring

Exercise 15 what I want to do is \(\frac{x(2 - y)}{x}\cdot(-1) + 2\) which = y but lean wouldn't let me because I still don't really understand how bracket scope works in lean it's not like normal scope in other languages unless I have no idea what I'm doing. Since one of those hypothesis rewrites to 0 you can freely multiply it by anything you want to produce a positive y as that will all get wiped out upon rewrite anyway.

Exercise 16 is of course impossible (no rational number exists that when squared is negative) but lean will let you prove it anyway using rewrites. If you want more exercises there's homework for this book/course in the git repository just don't post solutions anywhere or else prof's lock all their materials down to prevent cheating students.

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 unicode 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