Learning to talk to Xena

This page contains some general information about Lean, but parts of it are specific to undergraduates at Imperial College London.

Xena, our virtual undergraduate, only speaks one language, and this language isn’t English. I sometimes refer to this language as Lean, although a slightly more accurate name for it would be “Lean 3”. Someone with a computer science background might refer to it instead as the Calculus of Inductive Constructions. As a mathematician I find this name a little intimidating, so I will stick to Lean.

[Note that a previous version of the software is called Lean 2 — but Lean 2 and Lean 3 are not compatible, and when I talk about Lean I mean Lean 3. If I am being super-precise I might even say something like Lean 3.2.0 (update: I might now even say Lean 3.3.0).

If you want to see Xena reasoning about M1F (a.k.a the Imperial College course “Foundations of Analysis”) in this Lean language, you can take a look at her Github repository here, in the M1F directory. At the time of writing, all that is there is a statement of the first part of the first question of the first example sheet for M1F (although it’s high on my priority list to add more stuff). In human-readable mathematical language, the question is this:

Is the following statement true or false?

If x is a real number, then x^2-3x+2=0 \implies x=1.

The version that Xena understands currently looks like this:

¬ (∀ x : ℝ,(x*x(3:ℝ)*x+(2:ℝ)=(0:ℝ) x=(1:ℝ)))

This is a poorly-written sentence in Xena’s language. There are too many brackets, too many letter R’s, and there are other issues too. In general I feel that whilst what I have written is grammatically correct, it doesn’t flow very well. This is because I am still a beginner at speaking Xena’s language, and so still have a lot to learn. Over the summer of 2017 I made a concerted effort to learn Lean, using the tried and tested method of reading a couple of good books and doing the exercises. In fact the “books” were actually interactive web books. I started by glancing through this one:

Introduction to Lean, by Jeremy Avigad, Leonardo de Moura, Gabriel Ebner and Sebastian Ullrich.

and then I moved onto this one, which I read really thoroughly:

Theorem Proving in Lean, by Jeremy Avigad, Leonardo de Moura, and Soonho Kong.

I really enjoyed reading these books and doing the exercises. I found that even though the authors were computer scientists, they did not assume too much computer science background, and as a mathematician I could follow a great deal of what they were saying. The authors explain that these books are not quite complete yet. Indeed Lean is an ongoing project and much of the documentation is still evolving  — even the manual is still under construction!

However if you study at Imperial College London and are interested in learning to speak Lean, then you are welcome to try a completely different way of learning the language, which is simply by immersing yourself in it. This way, you don’t read any books at all, but you simply try to explain some mathematics to Xena. Those of you who have learnt other human languages in the past might have seen this technique before. When term starts I will run informal workshops where we can experiment together, trying to explain mathematics to Xena. For more details, see the M1F page on Blackboard, Imperial’s VLE. I will be teaching her M1F, the foundations of analysis course, and you can either help with this or try to teach her something else. Whatever you try to do, I will try to help. If anyone manages to explain to Xena the statement of one of the questions on an example sheet, or the statement of a theorem or a lemma in one of the courses they are studying, then they will have learnt something. When they have learnt it they might want to ask their personal tutor (who is probably a professional mathematician) whether the tutor can do it. If anyone manages to explain to Xena how to solve one of these questions, or to prove one of these lemmas, then they will have learnt something even better. Speaking from experience — it starts hard, but gets easier and easier. In fact it gets easier both for us and for Xena, because Xena’s language itself is evolving, as are the tactics that she knows to prove theorems. What is happening is that there are some very smart computer scientists out there who we don’t need to worry about at all and who are working on tuning Xena’s brain as we speak. As the term goes on, newer versions of Lean may appear (maybe by the end of term we will have Lean version 3.4.0 or higher), and for this and other reasons we might find that Xena can begin to take bigger steps on her own.

Let me next say a little about other resources.

When I was learning by reading books and doing exercises, initially I was using a version of Lean which is available online and which runs in your browser. However I quickly wanted a better end user experience, so I downloaded and installed Lean on a computer, following the instructions here . Lean is available for Windows, Mac and Unix. Initially I interacted with Lean using leanemacs (which was great for me because I have been using emacs for 20 years, but which might not be great for a new user). Later on I also started using the Lean plugin for Visual Studio Code, and this IDE might be much better suited for someone with no emacs experience; it has a much more modern interface which will look more familiar, and it does not use emacs’ obscure keyboard shortcuts.

Lean is a functional programming language, and before I embarked upon Lean I learnt something about Haskell. Haskell is a functional programming language which we teach to the first year computer science students at Imperial College (and those studying maths and computer science as a joint degree), and I knew pretty much nothing about it until earlier this year. I learnt what I know of Haskell by reading Learn You A Haskell For Great Good by Miran Lipovača, a book which I found both funny and interesting. However I am now not so sure that someone who wants to learn Lean needs to learn lots of Haskell. In fact I am not really sure that they need to know any Haskell at all.

Jeremy Avigad taught a course on mathematical proof and Lean at Carnegie Mellon university. Unfortunately the online notes for his course are written in Lean 2 (at the time of writing), so they can be a bit confusing because some of the code doesn’t work any more. Once you know what you’re doing, it’s not hard to translate the notes from Lean 2 to Lean 3, but if you’re still a learner then beware.

Finally, let me say a little about why one might want to learn Xena’s language. There are three reasons.

The first reason is that I think there is evidence that systems like Xena can learn quite a lot of mathematics if they are pushed. I believe (although I think I am currently very much in the minority amongst mathematicians) that one day in the future, serious research mathematicians, if they take the trouble to learn this language, will begin to actually use systems like Xena to help them with their own mathematics. In the early 1990s I saw serious research mathematicians stop what they were doing and learn TeX or LaTeX, so I know these big changes sometimes happen. If you have ever been stuck on a maths problem as part of a course you were studying (for example an A level or degree course) and have ended up just paging through your notes hopefully looking for some remark or theorem that might help you to do the question — Xena might one day be able to help you with that. She might be able to look through her database of theorems and examples, and suggest something useful. But first you have to learn how to talk to her. I wrote my PhD thesis in TeX. Maybe within a decade we will begin to find that people are writing their PhD theses in Lean. Maybe even, a long way in the future, Xena will be able to interact with some machine learning software and start trying to figure out the tricks that humans use to prove theorems, and maybe even try proving new theorems on her own. The thing is, to make this sort of thing happen, Xena needs a database of basic results to train on. That’s where we come in.

The second reason is that Xena checks everything. If a proof isn’t quite right, for example if it misses out a special case which needs checking, Xena will spot this. A proof that Xena understands is a proof which has been very carefully checked. Are you ever unsure whether an argument you give to solve a problem sheet question is right or not? If you lean Lean, you’ll be able to run the argument past Xena, and if she’s happy then you should have a lot of confidence in your argument. If she’s not, then either you have made a mistake, or you need to learn more about how to communicate in the language of Lean.

Experts in this area will point out that there are other computer proof assistants, such as Coq or Isabelle, which already have nice databases containing proofs of some (but by no means all!) undergraduate-level theorems and even some much harder theorems. So why create another one? My answer to this is that whilst I (in stark contrast to many mathematicians I know) personally believe that training computer systems to learn and check theorems is an important step for the future of mathematics, my impression is that the databases that already exist were designed, on the whole, by small teams of expert researchers whose job it was to design these databases. In particular the decisions they made about what to put in and what to leave out were being controlled by some ultimate goal which they needed for a publication or a research grant proposal. The Xena project is designed just for fun. There are no concrete must-achieve goals or deadlines for the project, it is currently a piece of blue sky research and any Imperial mathematics or JMC student can join the team and contribute as much or as little as they want, under no pressure from funding bodies and with no deadlines, and we can just see where it goes. In short: it is not the destination, it is the journey. Lean is a carefully-designed and very new language which has arguably learnt from some of the mistakes made by earlier systems. But that’s not the real point — the real point is that if we just wait for small teams of experts to write our database, we will have to wait for years and years and years. If I can teach undergraduates to write in this language, early on in their mathematical education, then maybe some of them will begin to find it second nature, and will become really skilled in speaking this language. If this happens, then we can simply let evolution decide whether this new skill is useful or not.

The third reason is — don’t you think it would be kind of fun to be part of a project where together we train a machine to learn how to do the questions in an undergraduate course? How many other undergraduate courses can we teach it?

Advertisements