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

# Overview

I’m going to explain how to install the current (bleeding edge) version of lean and mathlib, and set up a project directory on your (unix or windows or mac) computer where you can write lean files which use the newest features of mathlib. I’ll also explain at the end how to keep everything up to date.

We’ll start by briefly going through how to install git and vscode, and also msys2 on Windows (unlike unix and mac, windows doesn’t come with a command-line terminal, and msys2 is the one we’ll use). We’ll then download lean nightly from the lean website, and use the lean package manager to install mathlib; this method should ensure that the versions of mathlib and lean that we get will be compatible. Finally we’ll compile mathlib and then get the whole shebang working in vscode.

If you follow these instructions and they don’t work for you, please comment below and I will attempt to modify or clarify this document.

# Introduction (a.k.a “why do I want to do this?)

If you are a mathematician using Lean, you almost certainly want to use its maths library, mathlib (Note to self: justify this assertion by writing that blog post explaining all the stuff that is in mathlib). Furthermore, mathlib is currently (I write this in Dec 2017) undergoing growth at quite a rate — more stuff appears weekly, and the developers are open to accepting new code from people which fills in gaps in the library. I actively want to put some serious stuff into mathlib — modular forms, elliptic curves and so on, and over 2018 I will be working on this. I think mathlib has an exciting future.

Conclusion so far: we need to find a way (possibly involving some one-off hard work) to get mathlib installed once, and then we need to learn a simple method for keeping it updated. So let’s learn how to install Lean and mathlib on a computer. In this blog post I want to 100% cover Windows (10) and Linux (Ubuntu 16.04), the two operating systems I have easy access to, but hopefully (Ali or Julian — are you out there?) we will also get mac instructions up here before long.

# Preparation : installing other stuff.

tl;dr: Windows needs msys2, and every OS needs git and vscode.

## Windows : msys2

On Windows, you are going to need something called “msys2” (which will give you a terminal window so you can type commands in on a “command line” instead of just clicking on stuff). Either google for how to install msys2, or try this link:

Link to msys2 one click installer for Windows

Install it in whichever directory you like; you won’t need to remember where. My only piece of advice (which is a general piece of advice for installing anything at all on Windows) is that the full name of the directory where you install it has no spaces in. This is just generally good practice when doing command line stuff, because a space in a command line command generally means “we’re starting a new command or option now” rather than “hang on we haven’t even finished typing in the directory name yet, it just has a space in”. Click through, and the next thing you know you’ll have a black box where you can type in commands, not that you know any commands, because you use Windows.

## Windows, mac and linux : git

We’re going to need git.

#### Ubuntu

On Ubuntu linux you can install from the command line. Fire up a terminal and type

$git --version If it prints which version of git you have, you have git. If not then try $ sudo apt-get install git


#### Mac

On a mac, open a terminal and try

$git --version [NB don’t type the dollar sign]. If it prints which version of git you have, you have git. If not, you’ll have to install it. Either google for how to install git on a mac, or if you’re feeling lucky try here: git installer for osx See if git --version thing works now. If it doesn’t then you need to fix this. What is going on is that git is installed but your terminal doesn’t know where to look for it. You will need to change your PATH system variable so that it points to the right place. More than that I cannot say because I don’t have access to a mac and I don’t know whether things are joined up enough for this to work out of the box. #### Windows On Windows, open up an msys2 terminal and try $ git --version

[NB don’t type the dollar sign]. If it prints which version of git you have, you have git. If not, you’ll probably have to install it. Either google for how to install git on Windows, or if you’re feeling lucky try here:

Git installer for Windows

Get git installed, and my recommendation is that you install it in a directory whose full name does not contain any spaces. IMPORTANT: REMEMBER WHERE YOU INSTALLED IT — we will need this information in a second. Now click through all the masses of questions (the default options are fine) and then try that $git --version command in msys2 again. For me, it still doesn’t work, and that’s because msys2 doesn’t know where your git install is (in my case, this is because I put it in D:/Program_Files). I can fix this on my Windows machine by typing, in msys2, $ PATH=$PATH:/d/Program_Files/Git/bin [NB don’t type the first dollar sign but do type the other one]. The idea here is that the PATH variable contains a list of directories where the operating system looks for commands, and we’re telling it to look in the directory where the git command is installed. Now $ git --version works for me. You will have to change this line so that it contains the directory where you installed git, plus the extra /Git/bin bit at the end. Important note: if you foolishly installed git in C:/Program Files then you might have a problem because that path has got a space in. Another important note: if git --version doesn’t work (e.g. gives an error “git : command not found”) then the later stuff will not work either, so don’t bother continuing until this works. Once you’ve got it working, don’t close the msys2 terminal because it will probably reset the PATH variable (I guess).

### VSCode

We don’t need to worry about changing path variables for any of this. Just google for how to install vscode and install it on your system. Hint: try the link below:

Don’t worry about spaces in path names or anything. Just get it installed. We need to get it set up with the lean add-on etc but let’s leave that for now and come back to it later.

### Installing the nightly version of core Lean.

This paragraph works for all operating systems.

Go to the download page on the Lean website and download the “nightly” version of Lean for your operating system. Note that this is not something that you now need to compile or anything — it’s just one big compressed file containing a pre-compiled version of the Lean source code. Note that actually you could just download Lean stable instead, but then your version of mathlib will not be the most up to date version, and it might take you 30 lines of code to prove that $1<2$ (real numbers). Seriously.

You now have a zipped file containing all the lean source code and you need to extract this file to a directory somewhere. Decide where you are going to extract this file, and REMEMBER YOUR DECISION as we will need to tell both your terminal console and VSCode where the lean binary ends up. It can go anywhere, but I honestly recommend a directory whose name contains no spaces, especially if you are using Windows. Once it's all downloaded and extracted, fire up a file manager and have a look around. I've just installed Lean on this Windows 10 machine and I've put it in D:\Program_Files\lean-nightly-windows, which in retrospect might not have been so smart because now the actual lean.exe file on my machine is now at D:\Program_Files\lean-nightly-windows\lean-nightly-windows\bin\lean.exe. You might want to use a file explorer on your system to locate where your lean binary is, because this is what you’ll need to know later on.

We want lean to work in our terminal, and probably it won’t at the minute, because again the PATH variable probably doesn’t contain the directory . So on Windows I’m going to go back to my msys2 terminal and I’m going to type

$PATH=$PATH:/d/Program_Files/lean-nightly-windows/lean-nightly-windows/bin

On my ubuntu linux machine I have lean nightly installed in /home/buzzard/local/lean-nightly-linux and my path looks like

/home/buzzard/bin:/home/buzzard/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/home/buzzard/local/lean-nightly-linux/bin

where the operating system did all the earlier stuff and I added the last bit (in fact in my .profile file in my home directory I have the line

PATH="$PATH:$HOME/local/lean-nightly-linux/bin" 

which means I never have to change my PATH variable at all, it’s all done automatically.

Now (on any operating system) if I type

$lean --version I find I’m running Lean (version 3.3.1 as it happens, which doesn’t actually exist yet, we’re basically running a beta version of 3.3.1). On a mac you’re going to have to update your path variable, and probably it will be similar to how I did it in unix. The bottom line is that that this lean --version command should work in your terminal. Note that if lean --version gives “lean : command not found” then the stuff below will not work so you need to fix this now before you proceed. ### Make a new “project” and download and compile mathlib. The Lean files you write will be in your “project”, and your project will be in your project directory. Probably a sensible place for this is somewhere in your home directory. I would definitely avoid just making your project in whatever directory your terminal happens to be in currently — you will need to be able to find this project both in the command line and with your file explorer. In Windows I made a new directory called D:\Dad (this is not actually my Windows machine, and you can probably guess whose machine it is now) using the standard Windows file explorer. This isn’t my project directory — my project directory will live in this folder. I then navigate my way to this folder in msys2 with $ cd /d/Dad

This all works on unix and mac too. You can check where you are with

$pwd If you like, check that lean --version and git --version are still working. If everything is working, making our new project directory and installing mathlib in it should be easy. OK so I’m now in my terminal window, in the folder where I’m going to make my project directory and install mathlib. I do it like this: leanpkg new my_project cd my_project leanpkg add https://github.com/leanprover/mathlib leanpkg build  The first command might take some time to run. The second should be instant. The third might take some time to run — it’s installing mathlib. The fourth command should take ages to run and will just sit there not printing anything out if you’re using Windows — it’s compiling mathlib. You can check things are happening by using your file explorer to go into the _target/deps/mathlib directory in your project directory (this directory was created when you installed mathlib), and checking that some .olean files are appearing in various subdirectories. NB The first command might report “failed to start child process”. I have no idea what this means. The third command might tell you that you now have a detached head. Whilst this sounds alarming this might also be nothing to worry about. You just installed the current version of mathlib in your lean project. Note: the current version of mathlib on github is designed to run with the nightly version of lean. If you downloaded the stable version of lean (3.3.0) and the nightly version of mathlib, they won’t work with each other: you’ll have to figure out how to download the 3.3.0 version of mathlib, and this will have a lot less math in it than the current version. ### The moment of truth: getting it all to work in vscode. Fire up VSCode. Hit ctrl-comma (or File->Preferences->Settings) and make that User Settings file have a line which points to the lean binary file (e.g lean.exe on windows) which you installed when you installed lean nightly above. For example, on my Windows machine with the set-up I described above, I’m going to make it look like this:  { "lean.executablePath": "D:\\Program_Files\\lean-nightly-windows\\lean-nightly-windows\\bin\\lean" }  but if you’ve already used VSCode for a while then there might already be some stuff in this user settings file and you might end up wanting to make it look something like this:  { "files.exclude": { "**/.git": true, "**/.svn": true, "**/.hg": true, "**/CVS": true, "**/.DS_Store": true, "**/*.olean": true }, "lean.executablePath": "D:\\Program_Files\\lean-nightly-windows\\lean-nightly-windows\\bin\\lean", "window.zoomLevel": 2 }  Note the comma after the first close-squiggly-brackets above. Pro tip: if it’s in red, that’s bad. If lean.executablePath is in light blue and the D:\\Program_Files bit is in orange, that’s good. Any red is bad. All the quote stuff really matters. The two backslashes really matter. I know it was one backslash before but it’s two backslashes now. It’s Windows, you’re stuck with these issues. On unix or a mac it will look more like this:  "lean.executablePath": "/home/buzzard/local/lean-nightly-linux/bin/lean",  (in fact it looks exactly like this on my ubuntu install of vscode). You also need to install the lean extension for vscode. You do that like this. In the vertical bar on the left in Visual Studio Code, hover over the symbols until you find that one that says “Extensions” (it’s square, it’s at the bottom) and click on it. A list of popular extensions appears. Type lean in the search bar just above it. It should find an extension just called “lean”. Click “Install”. That’s it. OK now in VSCode try “File -> Open Folder” and open your project folder (so I’m opening D:\Dad\my_project). On the left (click the top left icon in that list of 5 icons if you don’t see it) you should now see your project name, and your project should currently contain something like 3 files and a directory (_target, .gitignore, leanpkg.path and leanpkg.toml). Those things were created when you used leanpkg to make your project directory. The secret is that leanpkg will have set up that path file so that it points to mathlib, and we just set up the VSCode user settings so they pointed to core lean, so we should now be all set. If you hover on the grey bar on the left where it says your project name, there’s a “new file” option. Click it and name your new file test.lean. Now put the following two lines in test.lean: import analysis.real #check real If there are orange bars on the left and/or right, Lean is thinking. Wait for the thinking to finish before panicking. If you decide to panic then one good way of panicking is pressing Ctrl-Shift-P and then typing “Lean: Restart”. If import is not underlined in red, and if you put your cursor on the “check” and get “R : Type” on the right hand side, you’re done. If not, ask for help. Either in the comments, or at the Lean gitter page (you will need to set up a github account, but you’ll need one of those anyway if you want to contribute to mathlib or to Xena’s library). ## Keeping everything up to date. If you have everything you need, then you have the option of not doing anything. But if in a few weeks or months from now there’s something that has just appeared in mathlib which you want, and which you don’t have, then you need to upgrade. If you are lucky, you don’t need to touch core lean. If you’re unlucky you need to upgrade core lean too. To upgrade core lean, just do exactly the same as you did when installing it the first time — go to the Lean downloads page, download the nightly, and unzip it in exactly the same place as before. You’re updated. To upgrade mathlib, fire up your terminal (msys2 if in Windows) and then get your PATH variable sorted out by making sure it includes the path to git and the path to Lean (you can check this by making sure $ git --version
and
$lean --version both work). Then just change into your project directory and simply type $ leanpkg upgrade
 \$ leanpkg build
Each of these commands might take some time (especially the second one). But this should do it.