Advertisements
Category Archives: undergrad maths
Lean in LaTeX
Patrick Massot wrote a formatter, which can turn Lean code into beautiful LaTeXxy html. The undergraduates and I have been formalising Imperial’s first real analysis course M1P1 in Lean. Put them together and you get a 21st century proof of … Continue reading
Blue-eyed islanders (guest post)
Thanks very much indeed to Chris Hughes, who has written up some thoughts on the blue-eyed islanders problem. Before we start, here’s the history. I (KMB) heard about this problem a few years ago, and thought it was cute, but … Continue reading
Posted in Learning Lean, M1F, undergrad maths
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
What is the Xena Project?
The current aims and ambitions of the Xena Project are twofold. 1) Digitise the curriculum. I would like to see the main definitions, theorems and proofs, and example sheet questions and solutions, in all of the undergraduate pure mathematics courses … Continue reading
Posted in General, Imperial, undergrad maths
8 Comments
Happy birthday Xena!
It was a year ago today that I emailed Inkeri Hibbins, a wonderful administrator at Imperial College London, and asked her if she could email all the Imperial maths and joint maths/computing undergraduates and tell them about my new Thursday … Continue reading
Posted in Imperial, M1F, undergrad maths
3 Comments
What is a uniform space? How some computer scientists think about completions.
This is post 2 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in an undergraduate mathematics course. These definitions play a rolein Lean because it’s important to set … Continue reading
Posted in undergrad maths
2 Comments
What is a filter? How some computer scientists think about limits.
This is post 1 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in a mathematics course. This one is on filters, and the next one will be on … Continue reading
Posted in undergrad maths
3 Comments
