Introduction

Who it is for. This guide is aimed at teachers who want to introduce Lean 4 to mathematics students who are used to writing proofs on paper but have no previous programming experience. No prior knowledge of computer science is required.

Philosophy of the course.

1. Lean is a proof notebook that talks back. You write an argument and the computer tells you, step by step, what is missing. It is presented as a patient interlocutor, not as a programming language.
2. Mathematics first, syntax later. Each topic starts from a proof the student already knows how to do on paper and translates it into Lean.
3. No installation at the beginning. The first three sessions can be done in the browser. Local installation comes when the student already wants to carry on alone.
4. You learn by reading the proof state. The central skill is not memorizing tactics, but reading the goals window (the infoview) the way one reads a blackboard.
5. Making mistakes is cheap. The red error is information, not a failure.

Structure. Eight topics of about 2 hours each (theory and practice mixed). Each topic has two parts: the content (what the student sees) and the teaching tips (notes for the teacher with key ideas, typical mistakes, ...).

Convention. All the examples start with import Mathlib.Tactic, Lean's library of tactics. The code blocks can be pasted as they are into the editor.

Read more…

Prove that if a sequence has two subsequences with different limits, then the sequence is not convergent.

To do this, complete the following theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

-- a converges to L
def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

-- The sequence a is convergent
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b is a subsequence of a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ : ℝ}

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SucConvergente a :=
by sorry

Read more…

A subsequence is obtained by applying an extraction function to the original sequence; that is, a strictly increasing function \(φ : ℕ \to ℕ\). For example, the subsequence \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] is obtained with the extraction function \(\varphi\) defined by \(\varphi(n) = 2n\).

The above definitions are formalized in Lean 4 as:

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) :=
  StrictMono φ

-- v is a subsequence of u.
def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

-- a is the limit of u.
def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

Prove that every subsequence of a convergent sequence converges to the same limit as the sequence.

To do this, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic

variable {u v : ℕ → ℝ}
variable {a : ℝ}

-- φ is an extraction function.
def extraction (φ : ℕ → ℕ) :=
  StrictMono φ

-- v is a subsequence of u.
def subsequence (v u : ℕ → ℝ) :=
  ∃ φ, extraction φ ∧ v = u ∘ φ

-- a is the limit of u.
def SeqLimit (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

example
  (hv : subsequence v u)
  (ha : SeqLimit u a)
  : SeqLimit v a :=
by sorry

Read more…

Prove that if the sequence \(a_{n}\) converges to \(L\) and \(M\) is an upper bound of \(a_{n}\) (that is, \(a_{n} ≤ M\) for all \(n\)), then \(L ≤ M\).

To do this, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

def IsUB (a : ℕ → ℝ) (M : ℝ) : Prop :=
  ∀ n, a n ≤ M

variable {a : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hM : IsUB a M)
  : L ≤ M :=
by sorry

Read more…

Prove that convergent sequences are Cauchy sequences.

To do this, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

def SeqLim (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SeqConv (u : ℕ → ℝ) :=
  ∃ a, SeqLim u a

def IsCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SeqConv u)
  : IsCauchy u :=
by sorry

Read more…

This week's challenge is to prove in Lean 4 that if the sequence \(aₙ\) converges to \(L\) and \(bₙ\) converges to \(M\), then \(aₙbₙ\) converges to \(LM\).

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

variable {a b c : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hc : ∀ n, c n = a n * b n)
  : SeqLim c (L * M) :=
by sorry

Read more…

El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión \(a_n\) es convergente, entonces \(a_n\) está acotada; es decir, existe un \(M ∈ ℝ\) tal que para todo \(n ∈ ℕ\), \(|a_n| ≤ M\).

Para ello, completar la siguiente teoría de Lean 4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Finset

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

def SeqBdd (a : ℕ → ℝ) : Prop :=
  ∃ M, ∀ n, |a n| ≤ M

variable (a : ℕ → ℝ)

example
  (ha : SeqConv a)
  : SeqBdd a :=
by sorry

Read more…

El reto de esta semana consiste en demostrar en Lean 4 que para todo \(n \in ℕ\), \(n(n+1)(2n+1)\) es divisible por \(6\).

Para ello, completar la siguiente teoría de Lean 4:

import Mathlib.Tactic

variable (n : ℕ)

example : 6 ∣ n * (n + 1) * (2 * n + 1) := by
by sorry

Read more…

El reto de esta semana consiste en demostrar en Lean 4 que existe un \(k ∈ ℕ\) tal que, para todo \(n \in ℕ\), \((n + k)^{2} ≤ 2^{n+k}\).

Para ello, completar la siguiente teoría de Lean 4:

import Mathlib.Tactic

example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) :=
by sorry

Read more…