Category Archives: Uncategorized
Lean Together 2021
A discussion of some of the talks from the Lean Together conference. Continue reading
Two types of universe for two types of mathematician
Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits I see I have done just enough to … Continue reading
Summer projects 2020
Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading
No errors.
Does your Lean file contain errors? Try and cut down. Continue reading
Counting binary relations: an apology
OK so this is really just another equality post. And an apology to the Imperial 1st years for teaching them badly. Let’s start with two questions. Q1) How many binary relations are there on a set with 2 elements? Q2) … Continue reading
Does anyone “know” a proof of Fermat’s Last Theorem?
So there’s a piece in Vice which quotes me as saying that I fear “all published maths is wrong”. Of course this is nonsense: indeed, as every mathematician knows, some published maths is wrong, but the vast majority of it … Continue reading
Equality part 3: canonical isomorphism.
I hadn’t planned on writing a third equality post, but my talk at Big Proof 2019 (see slides here) ended up having a huge section about “mathematician’s equality”, and I realised I had more to say about it. Here are … Continue reading
Perfectoid spaces!
Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! Patrick and Johan are professional mathematicians like me, not Imperial undergraduates, but I am sufficiently excited about the project that I couldn’t stop myself blogging … Continue reading
Happy pi day
Yesterday was pi day, and discussion of Lean’s support of pi came up on the chat. The discussion of pi is I think a great way of illustrating what Lean can and cannot do. To start with, “Lean has pi”. … Continue reading
