Category Archives: Imperial
Formalising Mathematics : workshop 7 — quotients
Is a quotient a set of equivalence classes? I think it’s something a bit more general than that. Continue reading
Formalising Mathematics : workshop 5 — filters
What is a filter on a set? I am kind of getting the hang of it now. Continue reading
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
Formalising mathematics : workshop 3 — sequences and limits
This week we’re going to do limits of sequences, of the kind you see in a 1st year analysis course. These are great fun to do in Lean. Because of Rob Lewis’ linarith tactic (which does the “and now this … Continue reading
Formalising mathematics : Workshop 2 — groups and subgroups
This is some notes on the second workshop in my Formalising Mathematics course, running as part of the EPSRC TCC. The Lean github repo is here. Groups and subgroups I start with an apology — there was far too much … Continue reading
Formalising mathematics : workshop 1 — logic, sets, functions, relations
An introduction to the material in workshop 1 of my “Formalising mathematics” course. Continue reading
Formalising mathematics: an introduction.
An introduction to the TCC course “Formalising Mathematics” Continue reading
The end of the summer.
It’s the end of the summer now, so it must finally be time to talk about the summer projects, and the things which happened since then. Continue reading
The Sphere Eversion Project
Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading
Summer projects 2020
Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading
Xena 