Tag Archives: Kenny Lau

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

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