Tag Archives: M1F

The inverse of a bijection.

Posted on June 11, 2019 by xenaproject

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading →

Posted in Learning Lean, M1F | Tagged , | 9 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