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 write up the proofs of all the results I stated as numbered theorems or lemmas in my M1F course. My M1F (introduction to proof) course has been one of my guides for what to work on in Lean. Of all the theorems I proved in M1F, de Moivre’s theorem (Theorem 3.2 of the course) is, I think, the only one which will need some work before it’s possible to verify it, the work in this case being a rigorous definition of the exponential function and its basic properties. I must confess that of all the other results, the hardest of them looks to me like the fundamental theorem of arithmetic — but Chris Hughes already did it! (and a whole bunch of the lemmas we needed along the way).

I feel like, other than the definitions of sine and cosine and exponential, and their basic properties, all of the M1F theorems should now be easily provable in Lean.


About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in M1F. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s