Ir al contenido principal

Publicaciones sobre RetoLean4 (publicaciones antiguas, página 2)

RSS feed (Lean4Challenge, en)

Canal RSS (RetoLean4, es)

También disponible en:

English (Lean4Challenge)

Reto 6: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L

Retos en Lean 4/Análisis/Límites

Demostrar el teorema del emparedado; es decir que si \(a_n\) y \(c_n\) convergen a \(L\) y \(a_n ≤ b_n \leq c_n\) para todo \(n\), entonces \(b_n\) converge a \(L\).

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

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

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

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L := by
  sorry

Leer más…

Reto 5: 5²ⁿ - 2³ⁿ es divisible por 17

Retos en Lean 4/Teoría de números/Inducción

Demostrar en Lean 4 que, 5²ⁿ - 2³ⁿ es divisible por 17 para todo número natural n.

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

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

variable (n : ℕ)

open Nat

example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by
  sorry

Leer más…

Reto 4: Existen infinitos números primos

Retos en Lean 4/Teoría de números/Primos

Demostrar que existen infinitos números primos.

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

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime.Defs

open Nat

example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  sorry

Leer más…

Reto 3: Si aₙ converge a L, entonces 2aₙ converge a 2L

Retos en Lean 4/Análisis/Límites

Demostrar con Lean 4 que si la sucesión \(aₙ\) converge a \(L\), entonces \(2aₙ\) converge a \(2L\).

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

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

variable {a : ℕ → ℝ}

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

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

Leer más…

Reto 2: La sucesión 1, -1, 1, -1,... no es convergente

Retos en Lean 4/Análisis/Límites

Demostrar que la sucesión definida por 1, -1, 1, -1,... no converge.

Para ello, se propone completar la siguiente demostración en Lean 4:

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

variable {a : ℕ → ℝ}

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

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

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SeqConv a :=
by sorry

Leer más…

Reto 1: La sucesión 1/n converge a 0

Retos en Lean 4/Análisis/Límites

En Lean, una sucesión \(a₀, a₁, a₂,...\) se puede representar mediante una función \(a : ℕ → ℝ\) de forma que \(a(n)\) es \(aₙ\).

Se define que \(L\) es el límite de la sucesión \(a\), por

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

Demostrar que si para todo \(n\), \(aₙ = 1/n\), entonces la sucesión \(a\) converge a 0.

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

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

variable (a : ℕ → ℝ)

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

example
  (ha : ∀ n, a n = 1 / n)
  : SeqLim a 0 :=
by sorry

Leer más…

Retos de demostración en Lean 4

Retos en Lean 4

He empezado a publicar la serie Retos matemáticos en Lean 4.

La dinámica es sencilla: cada semana propondré un problema matemático para que quienes estén interesados compartan sus soluciones en Lean 4.

Al terminar la semana publicaré las soluciones del reto, que seguirán este esquema:

  1. Una solución en lenguaje natural.
  2. Varias formalizaciones en Lean 4, de menos a más detalladas:
    1. La más automática, generalmente con grind.
    2. Otras con tácticas más específicas, como norm_num, ring, positivity o linarith.
    3. Una demostración final en la que esas tácticas se sustituyen por lemas concretos.

Con este refinamiento sucesivo se pretende que la demostración final se corresponda, en la medida de lo posible, con la escrita en lenguaje natural.