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.

Read more…

El reto consiste en demostrar en Lean 4 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

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

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

-- b es una subsucesión de a.
def subsucesion (b a : ℕ → ℝ) : Prop :=
  ∃ φ, extraccion φ ∧ b = a ∘ φ

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

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

Read more…

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 extraccion (φ : ℕ → ℕ) :=
  StrictMono φ

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

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

El reto de esta semana consiste en demostrar en Lean 4 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 extraccion (φ : ℕ → ℕ):=
  StrictMono φ

def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ

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

example
  (hv : subsucesion v u)
  (ha : LimSuc u a)
  : LimSuc v a :=
by sorry

Read more…

El reto de esta semana consiste en demostrar en Lean 4 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

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

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

example
  (ha : LimSuc a L)
  (hM : CotaSup a M)
  : L ≤ M :=
by sorry

Read more…

El reto de esta semana consiste en demostrar en Lean 4 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 LimSuc (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SucConvergente (u : ℕ → ℝ) :=
  ∃ a, LimSuc u a

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

example
  (h : SucConvergente u)
  : SucCauchy u :=
by sorry

Read more…

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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

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

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hc : ∀ n, c n = a n * b n)
  : LimSuc 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

def SucConvergente (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

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

variable (a : ℕ → ℝ)

example
  (ha : SucConvergente a)
  : SucAcotada 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…