Maths undergraduate example sheets

I’m teaching a course called M1F this term — the basic “introduction to proof” course which all first year maths (and joint maths/computing) students have to take at Imperial College London. The course is supposed to be managed via our VLE, but in practice this means that no other staff members can see what’s going on, so I also maintain a web page, which is here. The problem sheets will slowly appear over the course of the term.

One thing which is kind of obvious if you know about this sort of thing, but somehow I still find striking, is how incredibly varied in difficulty the problems are if you try to solve them in Lean. There seems to be barely any correlation between how difficult the questions are for a human and how difficult they are in Lean. Because of the way type theory works, questions involving integers, rationals and reals can get quite messy in Lean. Trivial observations such that “this integer is greater than 2 and less than 4, so it’s 3” can be hard to do in Lean, especially if you don’t know how to begin.

On the other hand, one thing I’ve noticed this year as I work through the questions in Lean for the second time in my life, is how much easier they are than the first time I tried them (this time last year). This is for two reasons. Firstly it’s because, obviously, I have a lot more Lean experience this time around. But secondly it’s really noticeable how many more tools there are — some are there because Mario Carneiro and others reacted to my frustration as a mathematician trying to use Lean and wrote specific tools in order to make my life easier, and some are there because members of the community are just writing tools anyway. In particular Rob Lewis wrote a tactic called linarith which tries to solve basic linear inequalities and I just noticed yesterday how much easier this can make my life. Here’s an example (it’s sheet 2 question 2).

A “largest element” of a set is an element which is greater than or equal to every element of . One of the questions I ask the students is to prove that the open interval has no largest element (exercise for students: why isn’t the largest element?).

The mathematical idea behind the solution is this: if is an element, then it’s not the largest element because the average of and 1 is larger. Looking back at the proof I wrote last year, it was 25 lines long and used exotic inbuilt theorems such as div_lt_of_mul_lt_of_pos, the statement that and implies (this is not surprising — one has to prove somehow…).

This year I'm putting up the Lean solutions in a github repository and this year the proof looks like this:

import data.real.basic
import tactic.linarith

def open_zero_one := {x : ℝ | 0 < x ∧ x < 1}

-- open_zero_one has no maximal element
theorem Q2 : ¬ (∃ m : ℝ, m ∈ open_zero_one ∧ 
                  ∀ x : ℝ, x ∈ open_zero_one → x ≤ m) :=
begin
  rintro ⟨m,⟨H1,H2⟩,Hx⟩,
  -- now apply max hypothesis to (m + 1) / 2.
  have H := Hx ((m + 1) / 2),
  -- Can only use the hypothesis if we know (m + 1) / 2 is in the interval.
  have Hav : (m + 1) / 2 ∈ open_zero_one,
    split,
      -- now 0 < m is a hypothesis and 0 < (m + 1) / 2 is the goal
      linarith, -- and this tactic does it
    -- similarly hypothesis m < 1 implies goal (m + 1) / 2 < 1
    linarith,
  -- now use that m is supposed to be the max.
  have Hwrong := H Hav, 
  -- hypothesis Hwrong (m + 1) / 2 <= m contradicts hypothesis m < 1.
  -- Contradictory hypos means we can even prove a false goal.
  linarith,
end

The proof is eight lines long (not counting the comment lines). Mario’s rintro tactic does all the introductory stuff and Rob’s linarith does all the trivial inequality argument; pretty much the only thing we have to do “manually” is have the idea that is relevant.

Advertisement