Presentación

A quién va dirigida. Esta guía está dirigida a profesores que deseen presentar Lean 4 a estudiantes de Matemáticas acostumbrados a demostrar en papel pero sin experiencia previa en programación. No se requiere ningún conocimiento previo de informática.

Filosofía del curso.

1. Lean es un cuaderno de demostraciones que contesta. Escribes un argumento y el ordenador te dice, paso a paso, qué te falta. Se presenta como un interlocutor paciente, no como un lenguaje de programación.
2. Primero matemáticas, luego sintaxis. Cada tema parte de una demostración que el estudiante ya sabe hacer en papel y la traduce a Lean.
3. Cero instalación al principio. Las tres primeras sesiones se pueden hacer en el navegador. La instalación local llega cuando el estudiante ya quiere seguir solo.
4. Se aprende leyendo el estado de la prueba. La habilidad central no es memorizar tácticas, sino leer la ventana de objetivos (el infoview) como quien lee una pizarra.
5. Equivocarse es barato. El error en rojo es información, no un fracaso.

Estructura. Ocho temas de unas 2 horas cada uno (teoría y práctica mezcladas). Cada tema tiene dos partes: el contenido (lo que ve el estudiante) y los consejos didácticos (notas para el profesor con ideas clave, errores típicos, ...).

Convención. Todos los ejemplos empiezan con import Mathlib.Tactic, la biblioteca de tácticas de Lean. Los bloques de código se pueden pegar tal cual en el editor.

Leer más…

Demostrar que si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente.

Para ello, completar la siguiente teoría:

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

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

-- La sucesión a es convergente
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ es una función de extracción.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b es una subsucesión de 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₂)
  : ¬SeqConv a :=
by sorry

Leer más…

Una subsucesión se obtiene aplicando a la sucesión original una función de extracción; es decir, una función \(φ : ℕ \to ℕ\) estrictamente creciente. Por ejemplo, la subsucesión \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] se obtiene con la función de extracción \(\varphi\) definida por \(\varphi(n) = 2n\).

Las definiciones anteriores se formalizan en Lean 4 como:

-- φ es una función de extracción.
def IsExtraction (φ : ℕ → ℕ) :=
  StrictMono φ

-- v es una subsucesión de u.
def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

-- a es el límite de u.
def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

Demostrar que toda subsucesión de una sucesión convergente converge al mismo límite que la sucesión.

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

import Mathlib.Data.Real.Basic

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

def IsExtraction (φ : ℕ → ℕ):=
  StrictMono φ

def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

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

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by sorry

Leer más…

Demostrar que si la sucesión \(a_{n}\) converge a \(L\) y \(M\) es una cota superior de \(a_{n}\) (es decir, \(a_{n} ≤ M\) para todo \(n\)), entonces \(L ≤ M\).

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

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

Leer más…

Demostrar que las sucesiones convergentes son sucesiones de Cauchy

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

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

Leer más…

El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(aₙ\) converge a \(L\) y \(bₙ\) converge a \(M\), entonces \(aₙbₙ\) converge a \(LM\).

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

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

Leer más…

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

Leer más…

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 sorry

Leer más…

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

Leer más…