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
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
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
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
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:
grind.norm_num, ring, positivity o linarith.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.