How To Prove It With Lean
Preface
About This Book
This book is intended to accompany my book How To Prove It: A Structured Approach, 3rd edition (henceforth called HTPI), which is published by Cambridge University Press. Although this book is self-contained, we will sometimes have occasion to refer to passages in HTPI, so this book will be easiest to understand if you have a copy of HTPI available to you.
HTPI explains a systematic approach to constructing mathematical proofs. The purpose of this book is to show you how to use a computer software package called Lean to help you master the techniques presented in HTPI. Lean is free software that is available for Windows, MacOS, and Unix computers. To get the most out of this book, you will need to download and install Lean on your computer. We will explain how to do that below. An alternative is to run Lean on the web using Gitpod; we also explain how to do that below.
The chapters and sections of this book are numbered to match the sections of HTPI to which they correspond. The first two chapters of HTPI cover preliminary topics in elementary logic and set theory that are needed to understand the proof techniques presented in later chapters. We assume that you are already familiar with that material (if not, go read those chapters in HTPI!), so Chapters 1 and 2 of this book will just briefly summarize the most important points. Those chapters are followed by an introduction to Lean that explains the basics of using Lean to write proofs. The presentation of proof techniques in HTPI begins in earnest in Chapter 3, so that is where we will begin to discuss how Lean can be used to master those techniques.
If you are reading this book online, then at the end of the title in the left margin you will find an icon that is a link to a pdf version of the book. Below that is a search box, which you can use to search for any word or phrase anywhere in the book. Below the search box is a list of the chapters of the book. Click on any chapter to go to that chapter. Within each chapter, a table of contents in the right margin lists the sections in that chapter. Again, you can go to any section by clicking on it. At the end of each chapter there are links to take you to the next or previous chapter.
About Lean
Lean is a kind of software package called a proof assistant. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.
Of course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.
Installing Lean
These instructions are based on the installation procedure that is described here. Alternative installation procedures can be found here.
We will be using Visual Studio Code to run Lean, so you will need to install VS Code first. VS Code is free and can be downloaded here.
You will also need the Lean package that accompanies this book, which can be downloaded from https://github.com/djvelleman/HTPILeanPackage. After following the link, click on the green “Code” button and, in the pop-up menu, select “Download ZIP”. Open the downloaded zip file to create a folder containing the HTPI Lean package. You can put this folder wherever you want on your computer.
Now open VS Code. You should see a window that looks something like this:
Click on the Extensions icon on the left side of the window, which is circled in red in the image above. That will bring up a list of available extensions:
In the Search Extensions in Marketplace field, type “lean4”. VS Code should find the Lean 4 extension and display it:
Click on “Install” to install the Lean 4 extension.
Next, in VS Code, select “Open Folder …” from the File menu and open the folder containing the HTPI Lean package that you downloaded earlier. Under the heading “Explorer” on the left side of the window, you should see a list of the files in the package. (If you don’t see the list, try clicking on the Explorer icon, circled in red below.)
Click on the file “Blank.lean” in the file list. You should see a warning that VS Code failed to start the ‘lean’ language server:
Click on the “Install Lean using Elan” button, and Lean should be installed. Then Lean should “build” the HTPI Lean package. This may take a while, but it only has to be done once.
If anything goes wrong, try quitting VS Code and restarting. Eventually your window should look like this:
If you don’t see the Infoview pane on the right side of the window, click on the “\(\forall\)” icon circled in red in the image above and select “Infoview: Toggle Infoview” from the popup menu.
Your installation is now complete.
Using Gitpod
To open the Lean package that accompanies this book in Gitpod, click here.
You will be prompted to create a Gitpod account if you don’t already have one; a free account gives you 50 hours of use per month. Then you will be asked to create a “workspace”. Click on “Continue”. It will take some time to create your workspace and initialize Lean, but this only needs to be done once. You will see messages about “cloning”, “building”, “downloading”, and “decompressing”. Then there will be messages about “building” files for the chapters of this book. (There will be some warning messages during this process, which you can ignore.) The last message will be “building HTPILib”. When that process is complete, you can click on the “X” on the right side of the lower part of the window to close the terminal pane containing the messages. You should see the HTPI Lean package, as described in the previous section. Later, you can return to the workspace you just created from your Gitpod user page.
About the HTPI Lean Package
For each chapter, starting with “Introduction to Lean,” the package has a file containing all Lean definitions and theorems from that chapter. There are also files containing all the exercises. In the exercise file for a chapter, all definitions and theorems from that chapter and all earlier chapters are available for use in solving the exercises.
The chapter files are inside the folder “HTPILib”. There is also one other file in that folder. All of these files are needed to make the package work. Do not edit the files in the HTPILib folder, or you will need to re-download the package.
License
This book is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License. This license allows you to share or adapt the book. In any adaptation, you must identify Daniel J. Velleman as the author, and you must also acknowledge that excerpts from How To Prove It, 3rd edition, copyright Daniel J. Velleman 2019, published by Cambridge University Press, are reprinted with the permission of Cambridge University Press. Each such excerpt is identified in this book with a parenthetical note “(HTPI p. …)” specifying the page of How To Prove It, 3rd edition from which the excerpt is taken. For further details, see the text of the license.
Acknowledgments
A number of people have provided advice, encouragement, and feedback about this project. In particular, I would like to thank Jeremy Avigad, Clayton Cafiero, François Dorais, Charles Hoskinson, Heather Macbeth, Pietro Monticone, and Ketil Wright.