Schemes!

Kenny Lau and I just defined a scheme in Lean!

The reason I am excited about this is that although most computer proof verification systems have plenty of definitions in, e.g. most of them seem to have stuff like groups and rings etc, the definition of a scheme is actually really complicated. Unlike the definition of a group, we had to actually prove theorems before we could formulate the definition of a scheme. Why is this? Not only does the definition rely on all sorts of auxiliary structures like a sheaf of rings on a topological space (which relies on definitions of presheaves of rings and of sets), the main issue is that a scheme must “locally look like the spectrum of a ring”, and to formulate this rigorously one has to define localizations of rings at multiplicative sets and prove a whole bunch of things about these localizations (almost all of this part of the project was done by Kenny).

My next goal is perfectoid spaces.

 

 

Advertisements
Posted in General | Leave a comment

Working with integers

The integers.

Lean has integers inbuilt as part of the core library. You can call them int if you want to be old skool, but if you type \Z (and then hit the space bar) in VS Code or emacs or the lean web editor you should get a nice looking .

A word of warning before we start — if you just type some number like 3, then Lean will by default assume that it is a natural number, and the natural number 3 is a different 3 to the integer 3 — that’s how type theory works. You can demand the integer 3 by writing (3:ℤ) (the brackets are essential).

Many basic operations on the integers are defined by recursion (which just means induction for definitions — we prove by induction and define by recursion). This means that secretly there is a computer program in the background which is running the show, complete with proofs of its beliefs. One consequence of this is that often to check explicit calculations using the magic words “dec_trivial” (which I think means “this is trivial, by decidability of equality on the integers”). For example


theorem easy : (4:ℤ) - (5:ℤ) = (-1:ℤ) := dec_trivial

[Just a brief reminder of how these things are thought about in type theory — the idea is that the statement 4-5=-1 is a type (it also has a type, which is Prop), “easy” is a new Lean term whose type is 4-5=-1, and dec_trivial is a computer program which has produced this term. If this still makes your head hurt, forget it.]

In short, “explicit” calculations with integers can
be done using dec_trivial. But what about simple lemmas? How do we prove that addition is commutative on the integers? Well, if you worked through the explicit proof that addition on the natural numbers was commutative, then you could imagine that it’s going to be some sort of delicate proof by induction. But fortunately this has all been done for you by the lean developers, and we can just invoke the theorem in the core lean library to check addition is commutative:


example : ∀ a b : ℤ, a + b = b + a := add_comm

Indeed there are lots of basic facts about the integers which are inbuilt into Lean — you can see a few more here or (same words, different presentation) here. I wrote that document. Let me know which version you prefer and I will write further such documents using the style you like best. Learning to navigate your way around the library is a very important skill, and one which I say a little more about below when I leave you to work on this stuff on your own.

Congruences.

Let’s now define what it means for two integers a and b to be congruent mod m. We know exactly what it means though — it just means that b-a is a multiple of m. And what does it mean for b-a to be a multiple of m? It means that there’s some integer n such that b-a=m*n. We know what subtraction and multiplication mean — they are inbuilt into Lean. So we have our definition. Let’s also add some notation for it. You can get the standard symbol by typing \== in Lean.


namespace xena

definition cong (a b m : ℤ) : Prop := ∃ n : ℤ, b - a = m * n

notation a ` ≡ ` b ` mod ` m  := cong a b m 

#check (7 ≡ 22 mod 5) 

end xena 

What does that #check mean? Unfortunately it doesn’t mean “check this is true” — it means “check this makes sense, and if it does, return its type”. If you click on the #check (and if you have the messages buffer open — click one of those symbols that looks like some white rectangular blocks in a pile on top of each other if you don’t) you will see 7 ≡ 22 mod 5 : Prop. So Lean is telling us that 7 ≡ 22 mod 5 is a Prop, in other words a true-false statement. It is not telling us whether it’s true or false though! Indeed, if you change the numbers to #check (7 ≡ 8 mod 5) or anything else, Lean will still happily report that it is a true-false statement.

Proving that congruences are true.

So how do we prove 7 ≡ 22 mod 5? Well it looks like some concrete statement involving only known integers, so maybe we can use dec_trivial to prove it.

example : 7 ≡ 22 mod 5 := dec_trivial -- fails!

Why does fail when things like subtraction of concrete integers succeeds? It’s because Lean is trying to check that there exists an integer n such that 5 * n is 15, and this is beyond dec_trivial‘s pay grade. The proof that 7 ≡ 22 mod 5 needs to read like this: “n=3 works, and the proof of this is trivial”. So how do we feed this information into Lean? Well, it turns out we do it like this:

example : 7 ≡ 22 mod 5 := ⟨3,dec_trivial⟩ -- works!

The pointy brackets on the right can be typeset with \< and \>. To prove something of the form ∃ n, H (“there exists n such that H is true”) we use ⟨n0,proof⟩, where n0 is our choice for n and proof is our proof that it works. In the case above, H is 22-7=5*3 and this is exactly the sort of thing that dec_trivial can produce a proof of.

Proving facts about congruences.

[NB we are going to be writing simple proofs, here, and I would recommend that you have taken a look at at least some of this older post about building the natural numbers before you go much further into this post here.]

We can only use dec_trivial when all the numbers are known. If we have variables then we need to use theorems. Let’s see this in action. Let’s try and prove that for a fixed m, congruence mod m is an equivalence relation. Let’s start with reflexivity. Even here we will find we need a theorem.

Reflexivity.

Let’s state the theorem.


namespace xena

definition cong (a b m : ℤ) : Prop := ∃ n : ℤ, b - a = m * n

notation a ` ≡ ` b ` mod ` m  := cong a b m 

theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin

end


end xena 

[or click here to try in the Lean Web Editor]. The begin/end block put us into “tactic mode”, which is by far my favourite lean mode. Our job is to fill in the blank between the begin and the end. Our code currently has an error, saying that we wrote “end” but we hadn’t finished yet (indeed we haven’t started).

We are trying to prove something of the form for all a, ... so we can start with intro a (don’t forget the comma afterwards) and now our goal becomes a ≡ a mod m. Now this is _actually_ notation, and whilst it is what Lean prints, our goal is actually the meaning of the notation, which is cong a a m. We can’t unfold notation, but we can
unfold that cong. We don’t have to (indeed when we’re finished try deleting that unfold and notice that the proof still works fine), but let’s do it anyway:


theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,

end

and if we put the cursor in that gap, we see that our goal is now
∃ (n : ℤ), a - a = m * n, and clearly our next step is going to be to prove this by suggesting that the reason it is true is because n=0 works. We saw in “term mode” (i.e. outside a begin/end block) that we could use some pointy brackets, and we could do something fancy-schmancy like refine ⟨0,_⟩ in tactic mode, but there’s an explicit tactic which will also work for us — the existsi tactic, which we can use to suggest the value to use in an exists statement. So let’s try

existsi (0:ℤ),

for the next line, and our goal now becomes

a - a = m * 0

That definitely looks true! But we can’t prove it with dec_trivial because there are variables in it. We need theorems, or automation (i.e. tactics which do heavy lifting). Here’s how to do it using theorems. First we observe that there’s a theorem called mul_zero which says that x*0=0 for any x. We can rewrite our goal using that theorem:

rw [mul_zero]

[NB what do you think the theorem that says that for all x, 0*x=0 is called? Can you see why this is a different theorem?]

Now we have to show that any integer, subtract itself, is zero. This theorem is called sub_self, and rewriting again is going to finish the job:

rw [sub_self]

If you followed along carefully and remembered all the commas, you now have


theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
existsi (0:ℤ),
rw [mul_zero],
rw [sub_self],
end

and no red lines any more, so we’re done.

There is however a nicer way to finish the job after our brilliant idea to set n=0, namely letting automation finish the job. For example


theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
existsi (0:ℤ),
simp
end

The simp tactic does all the easy calculations for us. It does use mul_zero to simplify the right hand side, but it doesn’t use sub_self for the left — those that are interested in seeing the lemmas it does use can type set_option trace.simplify true just before the line stating the theorem and then click on the simp line (which should now be underlined in green as it is producing output in the messages terminal now) and take a look at what it actually does.

Here’s everything in the Lean Web Editor.

Symmetry.

Here’s what we’re after. I would add this after reflexivity if I were you (but before end xena).


theorem cong_symm (m : ℤ) : ∀ a b : ℤ, (a ≡ b mod m) → (b ≡ a mod m) :=
begin

end

Notation is fickle; I had hoped we could get away without the brackets but we don’t seem to be able to. I guess they do clarify what’s going on.

After introing a and b, we can also intro our hypothesis H : a ≡ b mod m. Our hypotheses and goal should now look like this:


m a b : ℤ,
H : a ≡ b mod m
⊢ b ≡ a mod m

We now have a new problem with — instead of wanting to get rid of it in a goal, we want to use the fact that we have one in a hypothesis: we now have an _assumption_ that something exists (remember that H really says ∃ (n : ℤ), b - a = m * n as you will be able to see if you type

unfold cong at H,

). So how can we use this? Well we need to use a new command — cases.

cases H with t Ht,

destroys H and replaces it with an integer t (the integer that exists) and a new hypothesis Ht, the proof that t does what it is supposed to do. At this point our hypotheses and goal looks like this:


m a b t : ℤ,
Ht : b - a = m * t
⊢ b ≡ a mod m

In particular we now have four integers available to us, namely m, a, b, t, plus the hypothesis that b-a is m*t. Our goal is notation and, unfolding it in our heads (or even using unfold cong we see that it is ∃ (n : ℤ), a - b = m * n.

I think I might leave the rest to you.

Q1 Now comes the maths! We need to write existsi [something]. And once we’ve done that, we need to invoke some theorems. Here’s a useful one — mul_neg_eq_neg_mul_symm. Use #check mul_neg_eq_neg_mul_symm to find out what it does. You are going to be using rewrites and simps. Did you know that you can write rw ←Ht? If you didn’t know that, you might want to do the exercise about the natural numbers before attempting this one.

Transitivity.

Q2 Formulate and prove transitivity. Did you ever get stuck? Please let me know where. If you need to find lemmas in the lean libraries I would recommend typing #check and then some useful-looking keywords into Lean, and then hitting ctrl-space (and then escape and then ctrl-space again — I don’t know why but it works better the second time). This link might help you with keywords — make sure you know the difference between sub (a binary operator) and neg (a unary one). Remember also that A_of_B means “B implies A”.

More.

Q3 Can you now prove

theorem cong_is_equiv_reln (m : ℤ) : equivalence (λ a b, cong a b m) := sorry ?

Can you prove that if a ≡ b mod m and c ≡ d mod m then a + c ≡ b + d mod m? And what about a * c ≡ b * d mod m? Can you prove a ^ n ≡ b ^ n mod m? You might have trouble getting ^ to work — that is because core lean has been designed with an operator overloading issue which has not yet been fixed yet and might not be fixed for quite some time. Work your way around it with local infix ` ^ ` := monoid.pow at the top of your code [edit: curses! You need to have mathlib for this to work :-/ You need to get import algebra.group_power to work as well :-/]. If you can do all of these things, well done!

Posted in Learning Lean | 1 Comment

Recent student successes

Here’s what some of Imperial’s undergraduates have been doing.

Blue-eyed Islanders.

Chris Hughes typed up a solution to the blue eyed islanders problem! The question is here (M1F sheet 5) (question 6) (and also on Terry Tao’s blog here), and Chris’ solution is here.

I was told last year by an undergraduate that the official pdf solution I circulated to the students in 2016 was incomplete and the undergraduate did half-convince me of this. However I know for sure that Chris’ proof is complete, although philosophically there is still the issue of whether his formalisation of the problem is correct. This is an issue of interpretation rather than mathematics.

One of my first year tutees, Jin Su (Cris), told me the following great question: Let’s say I tell two of my tutees secret non-negative integers, and then I wrote two distinct non-negative integers on my whiteboard; one is the sum of the two secret integers, and the other one is not. I then take it in turns asking my tutees whether they know the other tutee’s number! Prove that eventually one of them will (truthfully) say “yes”.

I would imagine that this question can be dealt with in a similar manner. Mario Carneiro on the Lean gitter chat said that “usually knowledge is represented by a predicate of possible worlds rather than “things I know” ” . Can anyone (a) work out what he means and (b) reprove the Islanders problem using this approach or (c) solve Cris’ problem using any method at all?

Matrices.

Ellen Arlt proved that if R was a ring, then the set of n by n matrices over R was also a ring. Proving that inductive types have a complex structure (such as a ring structure) is harder than you might imagine; there were Lean issues which we had to solve. There were also mathematical issues which we had to solve; we had to learn how to manipulate finite sums (e.g. change order of summation), so we ended up learning a lot of generally useful skills. Ellen — please PR your work and I’ll link to it! A preliminary version is here but she finished the job yesterday. One thing that surprised me about the work was that she did not assume that the ring R was commutative! For sure it would be difficult to define the determinant of a matrix if the entries were in a non-commutative ring (even the case of a diagonal matrix is an issue). But the basic ring structure does not need commutativity of R, so I learnt something myself here.

Equivalence relations and congruences.

Julian Wykowski formalised several of the results which I proved in M1F about congruence of positive integers. In particular he proved that being congruent mod m was an equivalence relation, and various other important facts about congruences (such as how they behave well with respect to addition and multiplication). Julian’s work is here . It’s very clearly written; why not goof around with it online by following this link ?

The Exponential Function

Chris Hughes is formalising the exponential function and its basic properties, such as e^{x+y}=e^xe^y. This is very interesting to me because of all the theorems I proved in M1F, the de Moivre stuff is definitely the stuff that lies “furthest away from the axioms” and hence needs the most work.

Localisation of a ring.

Last but most definitely not least — Kenny Lau has formalised a sufficiently large amount of Atiyah–Macdonald’s book on commutative algebra to enable us to localise a commutative ring at a multiplicative set. We are now well on the way to defining affine schemes in Lean and once these are defined, defining a scheme in full generality should be not too much of a problem. Kenny’s work can be found here and in particular his localisation work is here although I believe it has just been accepted into mathlib! Well done Kenny!

Thank you to all students who have contributed recently.

 

Posted in Uncategorized | Leave a comment

What maths is already in Lean?

I sit around chatting to Imperial students on Thursday nights, and some of them will be writing Lean code. I encourage various people to work on various projects but in general I am quite happy to let people work on whatever they like. In the recent past I have encouraged people to prove that matrix multiplication is associative and distributive over matrix addition, that every prime which is 1 mod 4 is the sum of two squares, or that the spectrum of a commutative ring is a topological space. But in the past I have also encouraged people, foolishly, to do stuff which is already in core Lean or mathlib, and this was mainly because I had no good understanding of exactly what was there.

I decided to change this recently, by reading through all of core Lean and mathlib, and making notes on what was there. I now have a far clearer idea myself about what is there, and occasionally find myself telling students that something they are working on has already been done (of course this is no reason to stop working on it, but one might argue that there is still plenty of low-hanging fruit to work on).

So I decided to try and get some of my notes down on this blog, so that students can look for themselves. The current state of what I have managed to write is here, and I hope to update this page over the next few weeks until it contains a reasonable summary of most of the mathematics which Lean already knows. Once I have finished, it might be interesting to then continue by writing a list of all the mathematics which I think Lean could and should know, and which is accessible to undergraduates…

 

Posted in Uncategorized | 1 Comment

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.

Posted in M1F | Leave a comment

How to install mathlib and keep it up to date

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:

Link for installing vscode .

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.

Comments?

Let me know if it doesn’t work. Let me know if it’s explained badly. If it works for you — great, but I’m much more interested to hear if it doesn’t.

Posted in Technical assistance | 3 Comments