Interactive Theorem Proving in Lean

18th CICM, October 6-10 2025, University of Brasilia

import Mathlib.Data.Real.Basic

def Sequence (X : Type) : Type :=
  ℕ → X

def Sequence.isConvergent (s : Sequence ℝ) : Prop :=
  ∃ l : ℝ, ∀ ε > 0, ∃ n : ℕ, ∀ m : Nat, m ≥ n → |s m - l| < ε

def Sequence.isStationary (s : Sequence ℝ) : Prop :=
  ∃ a : ℝ, ∃ n : ℕ, ∀ m : Nat, m ≥ n → s m = a

theorem stationary_implies_convergent :
    ∀ (s : Sequence ℝ), s.isStationary → s.isConvergent :=
  by {
    intro s s_stationary
    -- dsimp [Sequence.isConvergent]
    -- dsimp [Sequence.isStationary] at s_stationary
    rcases s_stationary with ⟨a, n₀, ppty⟩
    exists a
    intro ε ε_pos
    exists n₀
    intro m m_ge_n₀
    rewrite [ppty m m_ge_n₀]
    simp only [sub_self, abs_zero]
    -- assumption
    exact ε_pos
  }

Goal of the workshop

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, using Lean as a programming language for this.

This workshop is part of the 18th Conference on Intelligent Computer Mathematics (CICM), to be held at the University of Brasilia, October 6-10, 2025.

Methodology

We cover the following topics and, for applications, we focus on examples extracted from Bachelor-level university mathematics (sequences of real numbers, divisibility theory, etc).

  • Inductive types, pattern-matching, induction.
  • Type families, Sigma-types, Pi-types.
  • Record types, formal representation of basic algebraic structures.

No prior programming skills are required to follow this workshop. Practice files are provided and no installation of Lean is necessary.

Contents

We do not assume familiarity with dependent types at the outset: our goal is to introduce them from scratch and show how they can be 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 programs, and we illustrate this notion with examples such as Euclidean division or the notion of prime element in a commutative ring without zero divisors.

Outline of the tutorial
Session Topic Practice files
1 Lean’s syntax and pattern-matching (1h)
2 Dependent type theory and applications to mathematics (2h)

References

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

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