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.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in M1F. Bookmark the permalink.

Leave a Reply

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

WordPress.com Logo

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

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s