Advertisements
Category Archives: Uncategorized
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
Posted in Uncategorized
Tagged Chris Hughes, Johan Commelin, Kenny Lau, Patrick Massot, perfectoid space, Ramon Fernandez Mir
4 Comments
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
2+2=4
I am interested in teaching and outreach, and often get asked to give talks to schoolkids. I gave one today, to a room full of year 10 kids (aged 14-15), and I showed them Lean. This was the youngest group … Continue reading
Posted in Uncategorized
4 Comments
A word on BIDMAS
Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure … Continue reading
Posted in Learning Lean, Uncategorized
Leave a comment
Formalising mathematics — a mathematician’s personal viewpoint.
Here is an overview of my current thoughts on formal proof verification systems in modern mathematics. 3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This … Continue reading
Tonbridge
Going down to Tonbridge to speak to the UK IMO squad. I will give one talk about why 144 is the largest square in the Fibonacci sequence, and then one talk about why 144 is the largest square in the … Continue reading
Posted in Uncategorized
Leave a comment
