.. _type_theory: What is this book about? ======================== There are many books (some extremely good) called things like "What is mathematics" or "an introduction to university mathematics", intended to bridge the gap between school and university mathematics. The books teach, often with many examples, what a mathematician means by a formal proof. We might see proofs that there are infinitely many primes, or that the square root of 2 is irrational, and go on to learn some basic examples of university-level concepts such as equivalence relations. Many such books exist already -- this is another one. What makes this book a bit different is that, whilst it is serving a similar role, it introduces a new tool which computer scientists have developed over the last twenty years or more and is now beginning to mature. This tool is the formal proof verification system. In short, computers can now check proofs. Currently, almost no mathematicians use these tools, probably for historical reasons. However these tools offer a huge advantage to the student: once they have learnt how to use them, the tools will check their own mathematical proofs! In particular, if a student types an attempted proof into one of these systems, they will *immediately know if it is correct*, because if it is not correct then the computer system will not be able to compile the code, and the student will see an error. In theory this sounds like a wonderful new teaching tool. However much work needs to be done. These systems are currently hard for mathematicians to learn. Established mathematics lecturers typically can not use these systems, because take up has been very low amongst mathematicians. What documentation there is is typically written by computer scientists, for computer scientists. There are several competing systems, each with their own advantages and disadvantages. Learning curves are very steep. In my opinion this needs to change, as soon as possible. The author envisages a future where mathematicians have engaged with these systems, and where using computer proof verification systems to help mathematicians with their work has become normal, from undergraduates to researchers. This book is an attempt to begin to realise that future. A lot of work remains to be done. How to read this book ===================== This book attempts to teach students how to do beginning university level mathematics using Lean, a formal proof verification system. Students can either install Lean on their own computers (it runs on Windows, Mac and Linux), or, if they don't want the hassle of doing this and are prepared for a slower and slightly less user-friendly experience, they can use Lean online without installing it. Lean sets up mathematics within the framework of dependent type theory. This is a theory which is completely alien to most mathematicians, who mostly either don't worry about foundational issues, or they use something called ZFC set theory, which is a different foundational system. It really does not matter which foundational system you use, ZFC set theory and dependent type theory can prove the same things, and the only real difference is the fiddly bit at the bottom involving how to actually build basic objects such as the natural numbers in the theory. The key point about the natural numbers is that induction works, and this is true both in ZFC set theory and dependent type theory, so at the end of the day it doesn't really matter what foundational system you use. The way I envisage students using this book is simply by diving in and trying the exercises. For each exercise sheet, there is (or, in most cases, will be) a short instructional video and a web page with some hints and tips on which tactics and/or theorems might be useful. The goal is to get students doing basic mathematics in Lean as soon as possible, starting with logic and working up to basic arguments with numbers, sets, functions, relations and so on. Later on, students might choose to read the appendix, where dependent type theory is described in a way which is hopefully comprehensible to mathematicians. To just jump straight in to Chapter 1, click :ref:`here `.