Category Archives: tactics

Formalising Mathematics : workshop 4 — topology

OK, an overview of this week: we’re doing topology. I was going to introduce filters but I decided to put them off for one more week, so this week it’s topology the way it is traditionally taught in mathematics departments. … Continue reading

Posted in formalising mathematics course, Learning Lean, tactics, undergrad maths | Leave a comment

Equality part 2: syntactic equality

Syntactic equality is yet another kind of equality. I am beginning to learn why it matters. Continue reading

Posted in Learning Lean, tactics | Tagged , | Leave a comment

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 … Continue reading

Posted in Imperial, Learning Lean, M1F, tactics, undergrad maths | Leave a comment

617 is prime

More number theory today. Clara List and Sangwoo Jo were trying to do a question from the third year number theory example sheet; to work out whether 605 was a square modulo 617. They decided to assume the law of … Continue reading

Posted in number theory, tactics | 4 Comments


The problem This post is about the equation . This special case of the binomial theorem is the sort of thing that we would expect incoming students at my university to know, or at least to be able to compute … Continue reading

Posted in General, Learning Lean, tactics | Leave a comment