Category Archives: M1F

Happy birthday Xena!

It was a year ago today that I emailed Inkeri Hibbins, a wonderful administrator at Imperial College London, and asked her if she could email all the Imperial maths and joint maths/computing undergraduates and tell them about my new Thursday … Continue reading

Posted in Imperial, M1F, undergrad maths | 3 Comments

Complex numbers! And M1F theorems.

Lean now has complex numbers! Now all we need is sine and cosine and we might be able to prove de Moivre’s theorem! The reason I’m interested in this is that I thought that it would be interesting project to … Continue reading

Posted in M1F | Leave a comment

Rational powers

Lean’s core library has no support for rational or real numbers šŸ˜¦ They are however in the maths library — or we can just make some fake real numbers and use them instead. — let’s define the real numbers to … Continue reading

Posted in Learning Lean, M1F | Leave a comment

Sheet 1 Q2,Q3

I’ve solved Q2 and Q3 of M1F Sheet 1 and pushed the solutions to github. Q4 I somehow want to persuade Xena to do herself, but I don’t quite know the best way to do this. These questions were much … Continue reading

Posted in M1F | Leave a comment

First question done!

I have finally typed up full proofs for Xena, for the first question of M1F sheet 1. Here are the questions in traditional PDF format: Example Sheet 1. Here’s a link to a live Lean session containing theĀ Solutions to all … Continue reading

Posted in M1F | Leave a comment