Tutorial Interactive Theorem Proving in Lean

            18th Conference on Intelligent Computer Mathematics
                                - CICM 2025 -
                             October 6-10, 2025
                               Brasilia, Brazil 
                     http://www.cicm-conference.org/2025

---------------------------------------------------------------------------------------- 
          
The goal of this half-a-day tutorial is to provide a training framework for
mathematical educators interested in the use of interactive theorem provers
in the classroom. We cover dependent sums and products, induction principles, 
and basic algebraic datatypes. For applications, we focus on examples
extracted from Bachelor-level university mathematics (groups and rings, basic
number theory, ordered structures).

Motivation

More and more mathematical educators are choosing to use interactive theorem provers
as a tool to teach their students how to write a proof. However, the practicality of this
approach strongly depends on the lecturer’s own field of expertise and prior programming
experience. With this tutorial, we wish to provide a framework to help mathematics
professors develop their coding skills and later teach their students to interact with a
proof assistant. The output is an introduction to interactive theorem proving for complete
beginners, using Lean 4 as a programming language for this.

Methodology

Notions of functional programming that we cover in Lean 4:
• Type families, Sigma-types, and Pi-types.
• Inductive types and dependent recursors.
• The use of record types to formalize algebraic structures.
A previous version of this tutorial, in the form of an 8h mini-course, was given at the
Max Planck Institute for Mathematics in the Sciences in Leipzig on 12-13 March 2025.
Practice files were provided to participants, who were able to use them directly on the
Lean 4 web server (no local installation required). The lecture slides and practice files for
that mini-course are available here:

https://matematiflo.github.io/LeanCompactCourse/
∗Faculty of Mathematics and Computer Science, Heidelberg University.

Contents

We do not assume familiarity with dependent types at the outset: our goal is to introduce
them and show how they are used to formalize existential and universal statements in
mathematics. This gives us an opportunity to discuss the calculus of predicates from the
constructive point of view, as well as the differences between this approach and classical
logic.

We also emphasize the importance of treating propositions as types and proofs as pro-
grams. While programmers may find this natural, experience shows that mathematicians
are often less comfortable than one might expect with the concept of proof relevance. We
illustrate this notion with examples such as Euclidean division or the infinitude of primes.

References

[1] Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Theorem
Proving in Lean 4. Available online.

[2] Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Xavier Généreux, Johannes
Hölzl, and Jannis Limperg. The Hitchhiker’s Guide to Logical Verification. Available
online, 2025.

Speaker
Florent Schaffhauser/Faculty of Mathematics and Computer Science, Heidelberg University.