Advertisements
Category Archives: undergrad maths
Lean does not (yet) have real manifolds.
Lean does not yet have real manifolds, but there has been recent progress. Continue reading
Advertisements
Posted in General, Imperial, undergrad maths
Tagged Agda, Bochner Integral, Coq, HOL-Light, Idris, Isabelle-HOL, Jeremy Avigad, Johan Commelin, lean, manifold, Mizar, Patrick Massot, Perfectoid Spaces, Sebastien Gouezel, theorem provers, UniMath, Zhouhang Zhou
7 Comments
M1F, Imperial undergraduates, and Lean
Abhimanyu Pallavi Sudhir, a current first year, has formalised the solutions to last year’s M1F final exam! Continue reading
Posted in M1F, undergrad maths
Tagged Abhimanyu Pallavi Sudhir, Chris Hughes, Kenny Lau, M1F
1 Comment
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?
Note (added June 2019); this (below) is an old blog post from 2018. You should really read the updated one here but I’ve left this original one just to preserve history. The current aims and ambitions of the Xena Project … Continue reading
Posted in General, Imperial, undergrad maths
8 Comments
