Category Archives: Uncategorized

2022 Xena Project undergraduate workshop

I have funding to run an undergraduate workshop! When? 26th to 30th September 2022 (the week before term starts for many people in the UK). What? A week-long in person workshop including a bunch of working on group projects in … Continue reading

Posted in Uncategorized | Leave a comment

New year, new teaching material

Imperial College has gone back to in-person teaching so I have 250 new subjects to experiment on, namely the new 1st year maths undergraduates. I’ve spent a few years now trying to figure out how best to teach maths undergraduates … Continue reading

Posted in Uncategorized | Tagged | 3 Comments

2021 Xena Summer Projects

So I spent July and August supervising mathematics undergraduates who were doing Lean projects in various areas of mathematics. Conformal maps, Euclid’s SAS theorem, nilpotent groups and the Radon-Nikodym theorem are just some of the topics I’ve been engaging with … Continue reading

Posted in Uncategorized | Leave a comment

Half a year of the Liquid Tensor Experiment: Amazing developments

[This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic Geometry lecture notes on joint work with Dustin … Continue reading

Posted in Uncategorized | Tagged , , | 22 Comments

Formalising Mathematics : workshop 8 — group cohomology

A brief description of group cohomology H^0 and H^1, plus links to how to formalise this stuff in Lean. Continue reading

Posted in Uncategorized | 5 Comments

Formalising Mathematics : workshop 6 — limits

I talked about limits of sequences of real numbers in workshop 3, but this week I come back to them, because this week we’ll see that the usual ten-line proof that if and then can be replaced by a two-line … Continue reading

Posted in Uncategorized | Leave a comment

Formalising mathematics: an introduction.

An introduction to the TCC course “Formalising Mathematics” Continue reading

Posted in formalising mathematics course, Uncategorized | 19 Comments

Lean Together 2021

A discussion of some of the talks from the Lean Together conference. Continue reading

Posted in Uncategorized | Tagged | 12 Comments

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