J.A. Alonso in Retos Matemáticos
El reto de esta semana consiste en demostrar con Lean4 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic
import Mathlib.Data.Nat.Prime.Defs
example
(n : ℕ) :
∃ p, n ≤ p ∧ Nat.Prime p :=
by sorry
El enunciado se encuentra en Lean 4 Web.
Las soluciones pueden publicarse hasta las 21:00 del domingo 7 de junio de 2026.
#RetoLean4 #31May26
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
#RetoLean4: Demostrar con Lean 4 que si aₙ converge a L, entonces 2aₙ converge a 2L.
https://t.me/Retos_Matematicos/109557/140007 #LeanProver #ITP #Math 
J.A. Alonso in Retos Matemáticos
El reto de esta semana consiste en demostrar con Lean 4 que si 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
example
(ha : LimSuc a L)
(hb : ∀ n, b n = 2 * a n)
: LimSuc b (2 * L) :=
by
sorry
El enunciado se encuentra en Lean 4 Web.
Las soluciones pueden publicarse hasta las 21:00 del domingo 31 de mayo de 2026.
#RetoLean4 #24May26
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
#RetoLean4: Demostrar con Lean 4 que la sucesión 1, -1, 1, -1, ... no es convergente.
https://t.me/Retos_Matematicos/109557/139918 #LeanProver #ITP #Math 
J.A. Alonso in Retos Matemáticos
En el reto de esta semana continuamos explorando la convergencia de sucesiones, retomando el trabajo de la semana anterior. El problema consiste en 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
def SucConv (a : ℕ → ℝ) : Prop :=
∃ L, LimSuc a L
example
(ha : ∀ n, a n = (-1) ^ n)
: ¬ SucConv a :=
by sorry
El enunciado completo se encuentra disponible en Lean 4 Web. Las soluciones pueden publicarse hasta las 21:00 del domingo 24 de mayo de 2026.
#RetoLean4 #17May26
J.A. Alonso in Retos Matemáticos
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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
example
(ha : ∀ n, a n = 1 / n)
: LimSuc a 0 :=
by sorry
Enlaces: enunciado y soluciones.
#RetoLean4 #10May26 #LimiteSucesiones
J.A. Alonso in Retos Matemáticos
Con este mensaje os propongo ampliar los "Retos matemáticos" con los "Retos matemáticos con Lean 4".
La dinámica sería la siguiente: cada semana se publicará un problema matemático, y quienes lo deseen podrán desarrollar soluciones en Lean 4 a lo largo de la semana, compartiéndolas en este subgrupo. El proceso será idéntico al de los "Retos matemáticos" actuales.
Además, junto al enunciado, se incluirán dos enlaces a Lean 4 Web:
+ Uno con el enunciado del reto.
+ Otro con las soluciones, para quienes prefieran consultarlas sin esperar.
A continuación, os presento el primer reto.
José A. Alonso