.. raw:: latex
\frontmatter
.. _introduction:
Preface
=======
About this book
---------------
This is a book dealing with how to write careful, rigorous mathematical proofs.
The book is paired with code in the computer formalization language
`Lean `__.
The book's focus is on technique, not on theory-building: rather few theorems are proved and then
referred back to later. Instead, the core of the book is in examples. Over two hundred problems
appear with solutions as examples in the text, and several hundred more problems appear without
solution as exercises for the reader. Each problem and each solution is presented both in standard
mathematical prose and in Lean (the book should be read with a computer open to the corresponding
file of Lean code),
and since these two "languages" are almost equally foreign for
students who are new to proofs, most solutions are annotated with informal commentary.
Why Lean?
---------
People have been expressing mathematical arguments in words for thousands of years, and mathematical
language is by now very standardized, with many conventions to let mathematicians communicate with
each other efficiently and unambiguously. The primary goal of this book is to teach you to read and
write standard mathematical English prose.
Computer systems called *interactive theorem provers* (also known as *proof assistants* or systems
for *formalization*) offer an alternative way to express a mathematical argument.
`Lean `_, an open-source project developed at Microsoft Research and
elsewhere since 2013, is one such system, but they have existed since
`the early days of computing `_.
Interactive theorem-proving systems such as Lean have become steadily easier to use over the
years, but they are not yet actually *easy* to use: they can be fussy and unforgiving, just like any
other computer programming language. So why does this book propose that you use such
a system in your first encounter with proofs?
First: Like it says on the tin, writing proofs in an interactive theorem prover is interactive. At
each point in your proof, you can see a visual representation of the *proof state*: what you know
(your *hypotheses*) and what you are currently working towards (your *goal(s)*).
If you are new to writing mathematical proofs, you may be surprised at how hard you find it to
distinguish hypotheses from goals on paper after a few steps alternating between forward and
backward reasoning, or how easily you lose track of one case in a case division.
Lean's live-updating visual representation of the proof state frees you from needing to keep this
in your working memory.
Second: Computer formalization systems, fussy unforgiving programming languages that they are, throw
syntax errors when you make a mistake. Feedback is instant and you can keep iterating until you
have something that works. Writing a solution in Lean ensures that it is completely correct:
no substitutions of an inequality under a minus sign, no divisions by zero, no terms dropped in
the algebra. This is especially useful in doing proof-based mathematics: make a small error
halfway through a calculus problem and the rest of the solution probably won't change much, but
make a small error halfway through a proof and the rest of the solution may be useless.
Finally: You interact with Lean using *tactics* which each perform a single step of a certain mode
of reasoning. The tactics which are taught in this textbook (some custom-written for this book)
each constitute a single permissible "atom" of reasoning in the mental world of the book.
This makes objective something which in a prose-only textbook can be subjective: what constitutes a
fully-detailed proof. What's more, the "atoms" I offer you are designed to nudge you toward
certain styles of mathematical argument structure [#]_ which are conventional in standard
mathematical prose but which students are often slow to adopt.
This is a book about mathematics which uses Lean as a tool. It is designed so that the learning
curve is flatter for the Lean than it is for the mathematics [#]_ -- partly by a careful
choice of exercises, and partly by writing in a
Lean "dialect" of my own, with a limited Lean vocabulary [#]_ which is just flexible enough for the
mathematical needs of the book. (A summary of the major differences can be
found in the appendix
:ref:`transitioning_to_regular_lean`.) My hope is that most of your intellectual effort in solving
the problems will be devoted to the mathematics, not to Lean's implementation details or
quirks of syntax.
Contents and prerequisites
--------------------------
You are ready to read this book if (1) you know high school algebra inside out and (2) you have
experience learning to carry out complicated mathematical algorithms. I have in mind, as a typical
reader, a first- or second-year university student who has just taken Calculus II. But no calculus
is actually used in this book.
The main novelty of this text is the "bilingual" presentation, juxtaposing prose mathematics with
Lean code. But the design choices enforced by this presentation have shaped the text in other ways.
:numref:`Chapter %s ` contains an unusually careful treatment
of "calculational proofs". These proofs are a natural starting point for the book because they
translate easily to Lean, but they are also worthy of attention as a topic which students at this
level often struggle with. [#]_
:numref:`Chapter %s ` and :numref:`Chapter %s `
constitute a slow march through the rules of
`natural deduction `_, solving problems about
:math:`\mathbb{N}`, :math:`\mathbb{Z}`, :math:`\mathbb{Q}` and :math:`\mathbb{R}` which feature
increasingly many of the logical connectives and quantifiers. The requirement to translate
everything to Lean keeps the book strictly honest through these chapters. The typical intro-to-proof
textbook does not have this guardrail, and will commonly make minor abuses here -- for example,
presenting a good example of a proof by cases which implicitly also uses a not-yet-covered proof
technique such as filling a witness to an existential.
Logic is not taught explicitly until :numref:`Chapter %s `, by which stage
readers will already be comfortable with the various logical connectives/quantifiers and with
translating mathematical statements back and forth between words and symbols. This permits the
logic chapter to be relatively brief, with a focus on the concept of logical equivalence (presented
primarily using natural deduction, to link with :numref:`Chapters %s ` and
:numref:`%s `, rather than using truth tables). [#]_
The other chapters of the book are more recognizable as the usual subject matter of a first
course on proofs. Sufficient familiarity with Lean has been established, and the mathematical presentation
is no longer constrained.
:numref:`Chapter %s ` covers the basic notions of elementary number theory.
This chapter uses only a limited toolbox of
reasoning techniques, to permit it to be placed as a break between
:numref:`Chapter %s ` and :numref:`Chapter %s `.
Number-theoretic definitions and theorems continue to appear as examples in subsequent
chapters, and the presentation of the subject concludes in :numref:`Chapter %s ` with
the big results of Greek mathematics: infinitude of primes, Euclid's lemma, and the irrationality of
the square root of two.
:numref:`Chapter %s ` covers induction. The treatment is fairly comprehensive, including
induction and recursion relative to various nontrivial well-founded relations on :math:`\mathbb{Z}`,
:math:`\mathbb{N}\times \mathbb{N}` and :math:`\mathbb{Z}\times \mathbb{Z}`.
Finally, :numref:`Chapters %s `, :numref:`%s ` and :numref:`%s ` cover
functions, sets, and relations, in that order -- we take the type-theoretic point of view that
functions are the primitive notion and sets and relations are defined as functions into
:math:`\left[\operatorname{true}/\operatorname{false}\right]`.
Note for instructors
---------------------
This book is based on lecture notes from a course I taught in Spring 2023 at Fordham University.
There were 20 students in the course, mostly first- and second-year students, with a median
background of Calculus II. Many but not all had also taken a first course in computer
programming.
The course had 75-minute classes, twice a week for 13 weeks, and in this time covered about 80% of
the material in this book. A typical class structure might look like this:
* 25 minutes traditional blackboard lecture;
* 5 minutes screenshare lecture doing the same problems in Lean;
* 20 minutes working in Lean in pairs, instructor circulating;
* 25 minutes traditional blackboard lecture, perhaps more theoretical than the first.
The homework assignments for the course are available on request.
They are relatively short (5-7 problems per week), but students were required to submit almost all
problems both in writing and in Lean. Most students required support in office hours or by email
to complete the homework assignments.
The course also featured oral examinations at the 5- and 10-week marks. These were 20-minute
one-on-one interviews assessing Lean fluency: students solved previously-unseen Lean exercises
(different exercises for each student), explaining their reasoning aloud. The grade breakdown for
the course was 25% homework, 20% oral examinations, and 55% traditional written examinations
(a midterm and a final, both completely Lean-free).
Clearly, the combination of in-class work with instructor circulating, homework support in office
hours and by email, and oral examinations adds up to a significant amount of time spent interacting
with individual (or small groups of) students. The student:staff ratio 20:1 was sustainable. I
suspect that to go beyond this ratio, one would need very strong students or an experienced and
enthusiastic TA.
The students ran Lean in a cloud development environment, to avoid needing to install Lean on their
own computers. I used `Gitpod `_ for this (an alternative is
`GitHub Codespaces `_) -- see the README of the book's
`code repository `_ for brief instructions on how to start
using Gitpod. The students' Lean homework was automatically graded using a
`Gradescope `_ auto-grader (an alternative is
`GitHub Classroom `_). The Lean community's
`teaching advice webpage `_ provides instructions
and troubleshooting for setting up this kind of course infrastructure.
Acknowledgements
----------------
My heartfelt thanks to
* Microsoft Research, for a `grant `_
which supported the writing of the book;
* My department at Fordham, for letting me teach the experimental course which this book grew from;
* The intrepid students in that course, Math 2001 L01 Spring 2023, for their enthusiasm and
resourcefulness;
* Matthew Hertz, for setting up the Sphinx infrastructure for the book and typesetting the first
chapters;
* The `mathlib community `_, and particularly Mario
Carneiro, Gabriel Ebner, Scott Morrison, Thomas Murrills and David Renshaw, for their work on the
Lean 3 to Lean 4 port in fall 2022 and winter 2023 prioritizing the parts of the library I needed
for the course;
* Mario Carneiro (also) for marathon hacking sessions which produced the most interesting custom
tactics used in the book;
* Jeremy Avigad, Rob Lewis and Patrick Massot, for sharing technical infrastructure for Lean-based
courses and for many conversations about the dream of teaching mathematics with Lean.
.. rubric:: Footnotes
.. [#] For example, the uses of calculation blocks for most algebraic reasoning, and a preference
for forward over backward reasoning.
.. [#] If you are looking for the reverse,
`Mathematics in Lean `_ is
the canonical introduction to mathematical Lean. But note that
that book expects more mathematical experience than this one does: writing idiomatic Lean code, even
to prove elementary statements, requires some mathematical maturity.
.. [#] The algebraic-reasoning tactic vocabulary of ``ring``, ``rw``,
``numbers`` (AKA ``norm_num``), ``rel`` (custom-written for this book but now in mathlib proper),
``extra`` (custom-written) and ``cancel`` (custom-written) suffices for pretty much all algebraic
reasoning over the integers, including nonlinear inequalities. The training in this vernacular
presented over the course of
:numref:`Sections %s ` - :numref:`%s ` pays off later,
by avoiding the need to invoke the endless lemmas such as
``mul_le_mul_of_nonneg_left``, ``pow_pos`` or ``le_of_pow_le_pow`` by name. Other custom
automation lightly streamlines work with induction principles, well-foundedness justifications,
product types, and sets.
In total, fewer than fifty lemmas are invoked by name in the book.
.. [#] It's in fact quite possible to get through the *equality*-heavy
reasoning of many intro-to-proof courses
without really mastering this mode of reasoning, but it's nearly impossible to reason about
*inequalities* without mastering calculational proofs, and students who don't pick up the skill in
an intro-to-proof course will find it come back to haunt them when they reach real analysis.
.. [#] The expert reader may enjoy the problems in :numref:`Section %s `, which introduces
classical reasoning; they are new (to my knowledge), and more elementary than the usual textbook
examples.