Interactive theorem proving in Lean

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 and methodology

We provide an introduction to interactive theorem proving, using the Lean proof assistant. We start with a presentation of the basics of dependent type theory, before moving on to projects involving formal proofs at the level of a Bachelor program in mathematics (sequences of real numbers, divisibility theory, etc.).

Pre-requisites

We assume no 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. No prior programming skills are required to follow this tutorial. Practice files will be provided and no installation of Lean is necessary.

Contents

We discuss the principles of intuitionistic type theory underlying proof assistants such as Lean, and we briefly outline the differences with classical logic and the set-theoretic perspective on foundations of mathematics. 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

Session	Topic	Practice files
1	Lean’s syntax
2	Propositions as types, proofs as programs
3	Dependent types
4	Algebraic structures