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:
  • First-order logic (FOL): the usual foundations of mathematics are Set Theory as a theory in First-order 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 real-life 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 real-world mathematics as well as form the basis for a real-world 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 super-human 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 safety-critical 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)
  • first-order 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.