-
-

Introduction

+
+

Preface

About this book

This is a book dealing with how to write careful, rigorous mathematical proofs. @@ -108,52 +109,9 @@

About this bookChapter 1 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. 1

-

Chapter 2 and Chapter 4 -constitute a slow march through the rules of -natural deduction, solving problems about -\(\mathbb{N}\), \(\mathbb{Z}\), \(\mathbb{Q}\) and \(\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 Chapter 5, 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 Chapters 2 and -4, rather than using truth tables). 2

-

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.

-

Chapter 3 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 -Chapter 2 and Chapter 4. -Number-theoretic definitions and theorems continue to appear as examples in subsequent -chapters, and the presentation of the subject concludes in Chapter 7 with -the big results of Greek mathematics: infinitude of primes, Euclid’s lemma, and the irrationality of -the square root of two.

-

Chapter 6 covers induction. The treatment is fairly comprehensive, including -induction and recursion relative to various nontrivial well-founded relations on \(\mathbb{Z}\), -\(\mathbb{N}\times \mathbb{N}\) and \(\mathbb{Z}\times \mathbb{Z}\).

-

Finally, Chapters 8, 9 and 10 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 -\(\left[\operatorname{true}/\operatorname{false}\right]\).

-
-

About Lean

+
+

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 @@ -187,18 +145,64 @@

About Lean3 which are conventional in standard +certain styles of mathematical argument structure 1 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 4 – partly by a careful +curve is flatter for the Lean than it is for the mathematics 2 – partly by a careful choice of exercises, and partly by writing in a -Lean “dialect” of my own, with a limited Lean vocabulary 5 which is just flexible enough for the +Lean “dialect” of my own, with a limited Lean vocabulary 3 which is just flexible enough for the mathematical needs of the book. (A summary of the major differences can be found in the appendix Transitioning to mainstream 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.

+

Chapter 1 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. 4

+

Chapter 2 and Chapter 4 +constitute a slow march through the rules of +natural deduction, solving problems about +\(\mathbb{N}\), \(\mathbb{Z}\), \(\mathbb{Q}\) and \(\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 Chapter 5, 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 Chapters 2 and +4, rather than using truth tables). 5

+

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.

+

Chapter 3 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 +Chapter 2 and Chapter 4. +Number-theoretic definitions and theorems continue to appear as examples in subsequent +chapters, and the presentation of the subject concludes in Chapter 7 with +the big results of Greek mathematics: infinitude of primes, Euclid’s lemma, and the irrationality of +the square root of two.

+

Chapter 6 covers induction. The treatment is fairly comprehensive, including +induction and recursion relative to various nontrivial well-founded relations on \(\mathbb{Z}\), +\(\mathbb{N}\times \mathbb{N}\) and \(\mathbb{Z}\times \mathbb{Z}\).

+

Finally, Chapters 8, 9 and 10 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 +\(\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. @@ -213,8 +217,8 @@

Note for instructors

20 minutes working in Lean in pairs, instructor circulating;

  • 25 minutes traditional blackboard lecture, perhaps more theoretical than the first.