Overview
Wednesday, Jan 4, 2023
About the course
Here we sketch the what, the why, the how, and the why now of this course.
What?
Broadly, our goals are the following
 Using programs (interactive theorem provers) to
 verify proofs of results,
 help in generating proofs.
 Proving correctness of programs;
 including writing the programs whose correctness we prove.
 Writing programs to find and/or verify proofs.
What do these mean?
To make sense of the above, we need to understand:
 What is a proof?
 What is a program?
Such questions form the foundations of mathematics and of computation.
There are different foundational systems, and we will look at two classes of these:
 Classical foundations:
 Firstorder logic (FOL): the usual foundations of mathematics are Set Theory as a theory in Firstorder logic.
 λcalculus: one of the equivalent formulations of the usual foundations of computation.
 Dependent Type Theory (DTT): foundations used by Lean that include both proofs and computations in a unified way.
In practice classical foundations are only useful in the small, i.e., for deductions using a relatively small set of axioms.
Indeed reallife mathematics is rigorous in only a local or domain specific fashion – we check that, for instance, calculations involving polynomials are correct in terms of rules and definitions for these, not in terms of polynomials represented in Set Theory.
On the other hand, the foundations building on Dependent Type theory can resemble realworld mathematics as well as form the basis for a realworld programming language.
What do theorem proving programs do?
Theorem proving programs vary in:
 the generality in which they work,
 how autonomous they are, and
 the complexity and scale they can handle.
They can be used for:
 Automation
 Formalization: more effort than a human proof.
 Tooling: helping find (possibly human) proofs.
 Software like Mathematica, SAGE, GAP handle specific mathematical problems with specific algorithms.
 General problems, but in the small, can be solved by
 SAT/SMT solvers for finite or special classes of infinite problems.
 FOL solvers such as Resolution Theorem Provers for general problems.
 Interactive theorem provers (ITPs) are used for general problems and in the large, but are typically not fully autonomous.
 AI/ML systems can be used to help with automation and can handle natural language, but are still not mature.
Why?
 It is obvious why we would want tooling or automation for mathematics.
 Since formalization takes work, it must be worth it.
 Formalization can also be done in other domains: software, hardware design, networking protocols, encryption schemes, even tax codes.
 An article by Patrick Massot gives a beautiful account of the motivation for formalization of mathematics.
Formalization of mathematics can:
 Give a superhuman level of guarantee of correctness.
 Allow abstraction and modularity when working with mathematics.
 Facilitate automation, both algorithmic and AI/ML based.
 Allow tooling for mathematics, such as semantic search.
 Facilitate collaboration.
 Facilitate using mathematics correctly in other domains (of mathematics).
Correctness

We obviously want to ensure high levels of correctness in all domains, i.e., with fewer and less serious errors.

This has to be balanced against the extra effort required.

In software, we use testing to minimize errors.

In mathematics, we use refereeing and other human checks.

Both these keep errors from spiralling out of control.

However, serious and unfixable errors are not uncommon.

In particular many papers in the Annals of Mathematics have unfixable errors.
 In the case of software, hardware, etc there are situations where it is worth taking a lot of effort to avoid (serious) errors.
 in safetycritical systems,
 in systems where a mistake is expensive to fix, such as chips,
 in systems software, where a bug is a vulnerability.
 As mathematics
 builds on other mathematics, and
 correctness is a defining property,
it is arguably worth applying at least the same standards as systems software.
How?
 We use Lean 4, which is a programming language and an interactive theorem prover.
 We will formalize mathematics, implement programs for mathematical computation, and prove their correctness.
 We will implement and formalize in Lean 4:
 a SAT solver (and maybe more)
 firstorder logic
 λcalculus
 We will see glimpses of AI/ML, including using tools under development.
Why now?
 Mature but still growing areas are:
 Experimental and Computational Mathematics,
 SAT/SMT solvers and their use in Mathematics.
 There is explosive growth in Lean and its mathematical library.
 There is even more explosive growth in AI/ML.
 There is great potential in
 interactive theorem proving
 interaction with AI/ML
 mathematical proofs of programs.