Tag Archives: Kenny Lau

Perfectoid spaces!

Posted on May 11, 2019 by xenaproject

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

Posted on May 6, 2019 by xenaproject

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