Organizers: David Gross (UoC), Davood Tehrani (RWTH). Time and venue: Wed 12pm (lecture), Wed 2pm (coding sessions), Seminar Room 0.01, Theoretical Physics Building, Zuelpicher Str. 77a, Cologne. Remote participation is possible.

Course description

Apparently, LLMs are the future of mathematics. Since summer 2026, these systems are solving long-standing open problems at an ever-increasing pace. This produces a new challenge: How can we be certain that the proposed proofs are correct?

In parallel with AI, a complementary technology has been making great strides in the past years: At the intersection of mathematical logic and theoretical computer science, the remarkable Curry-Howard correspondence states that one can interpret any mathematical deduction as a piece of code that computes a proof of its conclusion from proofs of its assumptions. Through this lens, a mathematical theorem is nothing but a program! What is more, software engineering methods (specifically: static type checking) can be used to certify the correctness of such programs, and hence of mathematical proofs. 

Many of the recent AI breakthroughs came with a “Lean formalization”, i.e. a formalized proof of correctness phrased using these ideas.

In this course, we will introduce theory and practice of formalizing mathematics in Lean.

Note: While AI is one motivation for our interest in formal methods, this course will teach you how to use these systems yourself. 

Topics:

• A beginner's guide to mathematical logic
  Proofs, deductive systems, constructivist vs classical logic, type theory, Curry-Howard correspondence
• 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.

Organization

• Lectures will take place Wednesdays from 12pm, followed by coding sessions from 2pm.
• If you want to participate online, please get in touch with us before the lecture starts.
• First lecture on Wed 14th of October.

Resources

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

Links

• https://lean-lang.org

Organization

• 6 ECTS points, involves a student project.