1. Introduction
Mathematics is done by pen and paper.
...Or is it?
In the past few years, there has been increasing interest in the mechanization of mathematics. This steampunk term refers to the use of sophisticated software packages that can express concepts of current research mathematics and verify proposed proofs for correctness.
These systems are referred to as proof assistants. That is a bit of a misnomer: They will not do very much to help you find a proof. To a beginner, they feel more like proof opponents: Like an extremely pedantic colleague who questions every step of an argument you suggest. Currently, getting one of these systems to accept your proof is considerably more work than writing it out on paper to accepted standards of rigor.
Despite these difficulties, the future of mathematics may well be mechanized. Indeed:
-
The leading systems come with fast-growing libraries of formalized results, on which projects can build. This will reduce the friction in the future.
-
They enable large-scale collaborations. The proof assistant can verify that individual contributions can be trusted, and that they cleanly fit together.
-
Large language models (the technology behind services like ChatGPT) can show stunning signs of creativity, but are also notoriously unreliable. An obvious strategy is to couple creative LLMs with pedantic proof verifiers. This combination might soon be too powerful to ignore
For this reason, getting acquainted with computer proof assistants seems like a good use of ones time. What is more, it is a hands-on way to learn some logic and think about the foundations of mathematics.
1.1. This course
In this course, we will
-
Recall some basics of mathematical logic
-
Introduce the Lean system from the bottom up
-
Implement a non-trivial project
As a project, we have chosen to prove the undecidability of the halting problem, a central result in computability theory.
Textbook proofs usually only sketch the result, and appeal to the reader's intuition to argue that certain constructions can be realized -- most notably if-then-else--type control flows. If you want to convince the Lean proof checker, such hand-waving is right out! We will therefore implement an complete interpreter for the small (but Turing-complete) programming language BF, and then prove unconditionally that it cannot decide its own halting problem.
As a byproduct, we will see how to
-
reason rigorously about computer programs.
1.1.1. Notes
-
OK, BF isn't the full name of the language. Too juvenile for you? Well, that's what I thought initially. But I've come around: For our purposes (but probably not for much else...) the language hits a sweet spot between simplicity and expressivity.
1.1.2. Communication styles
This course is jointly offered by the math and the physics department. Communication styles differ between the two fields.
Here's an analogy. Say you want to transmit this image
over a slow internet connection. Some encodings (such as the PNG format) are pixel-by-pixel. A partially-transferred file would thus appear as a perfectly completed part, followed by an empty region:
Other encodings (such as JPG) store image data in the Fourier basis. This allows for progressive rendering, where low-frequency components are sent over the wire first. Thus you get a full, but blurry image immediately, with the finer details appearing only later:
In this analogy, physics is JPG. We tell a complete story early on, but accept gaps and minor inconsistencies that may be resolved only later (and, well, sometimes never). For example, we're happy to build an entire theory on a formula that involves multiplying unbounded operators -- without mentioning that such products are well-defined only after having identified a common domain of definition, the choice of which isn't obvious at all.
Math is PNG. Using imprecise definitions at any point or making statements that are incompatible, even only in remote edge cases, is tantamount to quitting polite society. If this means that the full picture will come into view only later, that's considered a price worth paying.
Both styles will mix in the course. If that ever doesn't work for you, do speak up!