Organizers: David Gross, Frank Vallentin, Davood Therani, Marc Zimmermann. Time and venue: Thu 10am, Mathematical Institute, Weyertal 86-90, Seminar Room 1, ground floor.

Course description

A mathematical proof is basically a sequence of logical steps that shows why something is true. But how can we really check if such a sequence is a correct proof?

In the past, students of mathematics were trained to carefully read and write proofs — and to judge whether they are correct. Today, however, things are changing: more and more proofs are created with the help of computers. Some of these proofs rely on huge, complicated calculations that no human could ever fully check by hand. On top of that, large language models are being explored for generating proofs, but they often make mistakes (so-called hallucinations) and are not (yet?) reliable tools for professional mathematics.

One promising way to deal with this challenge is to use proof assistants. These are special computer programs designed to verify mathematical proofs with complete certainty.

In this course, we will first look at some of the logical foundations behind formalized mathematics, and then implement a non-trivial project.

Theoretical topics include:

• Propositional logic
  Why checking satisfiability is an NP-hard problem, but also why modern SAT-solvers can handle surprisingly large problems
• First-order logic
  Completeness: every valid statement can, in principle, be proven, Incompleteness: satisfiability cannot be decided in general
• Model theory
  A look at why the first-order theory of real closed fields is decidable

On the practical side, we will:

• Introduce the Lean system
  We will cover design principles and syntax from the bottom up
• Formalize a non-trivial proof
  As a hands-on project, we will formally prove the undecidability of the halting problem, a central result in computability theory. This includes the implementation of a bare-bones interpreter of a small (but computationally universal) programming language. As a by-product, we will see how to…
• …reason rigorously about computer programs

The course assumes neither prior exposure to mathematical logic nor programming experience.

Resources

• Some preliminary notes, with a high-level overview over some of the concepts we will cover.

Links

1. Terence Tao - Machine-Assisted Proofs (https://www.ams.org//journals/notices/202501/noti3041/noti3041.html)
2. Kevin Buzzard - What is the point of computers? A question for pure mathematicians (https://arxiv.org/pdf/2112.11598v2)
3. https://lean-lang.org

Organization

• 6 ECTS points, involves a student project.
• For integration into Physics MSc areas of specialization, contact David Gross.