Resources

Textbook

Our primary textbook is An Infinite Descent into Pure Mathematics by Clive Newstead. This book is freely available (choose version 0.4 the “stable download”). We shall follow this book closely. Note that this book is under development and the author would like feedback, constructive suggestions or comments based on your experience reading the text.

An optional secondary resource is How To Prove It: A Structured Approach by Daniel J. Velleman. This book was used as the course text in the previous iteration of this class. We will not follows this book, but you can find in there a wealth of examples and exercises if you need more practice.

Lean

We use the Lean theorem prover to interact with a computer when writing our mathematical proofs. This interaction consists of essentially four parts:

For checking the validity of our proofs;
For formalizing and digitizing our proofs;
For getting feedback and assistance from Lean to help us with completing our proofs;
For achieving a deeper understanding of some aspects of our pen-and-paper proofs by formalizing them;

At its core, Lean is what is known as a type checker. This means that we can write expressions and ask the system to check that they are well formed, and also ask the system to tell us what type of object they denote.

The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. The library also contains definitions useful for programming. This project is very active, with many regular contributors and daily activity. To get most out of learning Lean join this community.

The world of Lean proofs is the world of computers and programmes and is different than the world of pen-and-paper proofs as soon you will realize. In the world of Lean, parsimony is the moral dictum and verbosity is prohibited by structural design: Lean does not let us to write everything, even if it might make sense subjectively. We first have to understand the language of Lean to be able to talk to it. What I hope I get across is the contrast between Lean proofs and pen-and-paper proofs. While the second medium offers more freedom, the structural constraints of the first medium makes us appreciate that freedom even more, and honor it by being clear, concise, upright, and upfront in our mathematical communications.

Installing Lean

Lean installation guide

Alternatively, use the web editor

For the best user experience, I recommend installing Lean on your computer. Instructions on how to install Lean and “mathlibtools”, tools which will make doing mathematics in Lean 3 much easier, then head on over to the installation page on the Lean community website. Alternatively, you can use the web editor but you need internet access (). You can copy and paste the code of each lesson into the web editor. Note that it takes a few seconds for the web editor to load.

You can find more information, including very user-friendly installation guides and tutorials on Lean wesbite.

Lean installation guide

For viewing and editing lean code files you can use your favourite text editor. I recommend VSCode or Sublime Text.

Lean tactics

Getting Started with Lean

After the installation, you need to run leanproject new MATH301.This will create a directory with the name “MATH301”. Go to the ./src subdirectory (of MATH301), make an empty file, name it and save it in ./src (say prop.lean), and then copy-paste the content of Lean Lab lessons (say the lesson on propositional logic from https://introproofs.github.io/s22/prop_logic_nat_ded/code/) in your new file prop.lean. Save your file with a .lean extension in the ./src subdirectory of your project directory (with Command+Shift+S). Then open the entire directory with VSCode (either open VSCode first and then open folder, or via terminal from the directory MATH301 type the command code). There is an “info view” button on the top bar of VSCode (alternatively with Command+Shift+Enter) to interact with Lean.

Some big picture introduction to Lean:

Jeremy Avigad’s talk at the Topos Institute where he discusses some of the main aspects to the formalization of mathematics in Lean: Formal mathematics, dependent type theory, and the Topos Institute. You can also see the slides of this talk.
“What is the point of computers? A question for pure mathematicians”, Kevin Buzzard
Jason Rute’s talk at Harvard CMSA: Neural Theorem Proving in Lean using Proof Artifact Co-training and Language Models
Solving (Some) Formal Math Olympiad Problems

Lean Textbooks

For further reading, I recommend the following textbooks:

LaTeX

It is encouraged, but not required, that you use LaTeX for typesetting your homework assignments. LaTex is a powerful markup language for typing up mathematics and is used in many technical fields. Appendix D of our textbook has a nice introduction to the basic features of LaTeX. I will make homework files available in LaTex format so you can start using it right away. If this is your first time using LaTeX, I recommend that you start by using an online editor (e.g. Overleaf).

There are also offline TeX editors which you can install on your computer:

Tex editors: TeXstudio
Texmaker

Here are some guides to the basic elements of LaTeX:

If you are interested in pushing your LaTeX skills further, the best place on the web for Q&A about LaTeX is tex.stackexchange.

Fun Stuff

VISUALIZE CODE EXECUTION Adopt a Polyhedron!