# Category Archives: M1F

## Induction on equality

In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. Continue reading

Posted in M1F, M40001, Type theory, undergrad maths | Tagged , | 8 Comments

## Formalising Mathematics : workshop 7 — quotients

Is a quotient a set of equivalence classes? I think it’s something a bit more general than that. Continue reading

| | 7 Comments

## Division by zero in type theory: a FAQ

How can a theorem prover use the convention that 1/0=0 and still be consistent? Continue reading

Posted in Learning Lean, M1F, M40001, Type theory, undergrad maths | Tagged , | 12 Comments

## The inverse of a bijection.

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

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

## Blue-eyed islanders (guest post)

Thanks very much indeed to Chris Hughes, who has written up some thoughts on the blue-eyed islanders problem. Before we start, here’s the history. I (KMB) heard about this problem a few years ago, and thought it was cute, but … Continue reading

Posted in Learning Lean, M1F, undergrad maths | Leave a comment

## Maths undergraduate example sheets

I’m teaching a course called M1F this term — the basic “introduction to proof” course which all first year maths (and joint maths/computing) students have to take at Imperial College London. The course is supposed to be managed via our … Continue reading

Posted in Imperial, Learning Lean, M1F, tactics, undergrad maths | Leave a comment

## 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