Category Archives: Uncategorized

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

Posted in Uncategorized | Tagged , , | 9 Comments

Summer projects 2020

Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading

Posted in Imperial, Learning Lean, Uncategorized, undergrad maths | Tagged , | 2 Comments

No errors.

Does your Lean file contain errors? Try and cut down. Continue reading

Posted in Learning Lean, Technical assistance, Uncategorized | Tagged , , , | Leave a comment

Rigorous mathematics

What is rigorous mathematics? Jaffe and Quinn have some ideas, which I re-interpret a little. Continue reading

Posted in rigour, Uncategorized | Tagged , , , , , , , , , , , , , , , , , , , , | 13 Comments

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

Posted in Uncategorized | Tagged , , | 5 Comments

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

Posted in Uncategorized | Tagged , , , | 9 Comments

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

Posted in Uncategorized | Tagged , | 14 Comments

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 , , , , , | 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

Posted in Uncategorized | Tagged , | 2 Comments


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