#RetoLean4
LightNews LightNews
jalonso.eurosky.social
Weekly reads: Oct 19 – Oct 25, 2026.

🇬🇧 English: jaalonso.github.io/vestigium/en...

🇪🇸 Spanish: jaalonso.github.io/vestigium/po...

#AI #AI4Math #ITP #Lean4Challenge #LeanProver #Logic #LogicProgramming #Math #Prolog #RetoLean4
Weekly reads: Oct 19 – Oct 25, 2026
Here are the 42 reads I shared on Mastodon this past week. This week's main thread is, once again, the future of mathematics in the age of AI. Most of the AI4Math reads come from the Proofs and Prompt
jaalonso.github.io
October 26, 2026 at 7:28 AM
jalonso.eurosky.social
Reto 24 de Lean 4: La sucesión 1, -1, 1, -1,... no es convergente (usando el Reto 22). jaalonso.github.io/calculemus/p...

#RetoLean4 #LeanProver #ITP #Math
October 20, 2026 at 2:43 PM
jalonso.eurosky.social
Soluciones del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. jaalonso.github.io/calculemus/p...

#RetoLean4 #LeanProver #ITP #Mat
October 20, 2026 at 2:39 PM
jalonso.eurosky.social
Weekly reads: Oct 12 – Oct 18, 2026. jaalonso.github.io/vestigium/en...

#AI #AI4Math #ITP #Lean4Challenge #LeanProver #Math #RetoLean4
Weekly reads: Oct 12 – Oct 18, 2026
Here are the 20 reads I shared on Mastodon this past week. This week's main thread is the role of AI in mathematical practice and research ethics. Most of the AI4Math reads come from the Proofs and Pr
jaalonso.github.io
October 20, 2026 at 10:06 AM
jalonso.eurosky.social
Enunciado del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. jaalonso.github.io/calculemus/p...

#RetoLean4 #LeanProver #ITP #Math
Reto 23: La sucesión constante aₙ = L converge a L
El reto de esta semana consiste en demostrar en Lean 4 que la sucesión constante (a_{n} = L) converge a (L). Para ello, completar la siguiente teoría: import Mathlib.Tactic def LimSuc (a : ℕ → ℝ) (L
jaalonso.github.io
October 12, 2026 at 4:59 PM
jalonso.eurosky.social
Soluciones del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. jaalonso.github.io/calculemus/p... #RetoLean4

#LeanProver #ITP #Math
Reto 22: Subsucesiones con límites distintos implican no convergencia
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 Math
jaalonso.github.io
October 12, 2026 at 4:56 PM
jalonso.eurosky.social
Weekly reads: Oct 5 – Oct 11, 2026. jaalonso.github.io/vestigium/po...

#AI4Math #Autoformalization #CAS #FunctionalProgramming #Haskell #IsabelleHOL #ITP #LeanProver #Logic #Math #RetoLean4 #RocqProver
Weekly reads: Oct 5 – Oct 11, 2026
Here are the 38 reads I shared on Mastodon this past week. This week's main thread is the impact of AI on mathematics. Terence Tao ("Math 2.0"), Jeremy Avigad, Christian Szegedy and Quanta Magazine ea
jaalonso.github.io
October 12, 2026 at 10:44 AM
jalonso.eurosky.social
Enunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente.

#RetoLean4 #LeanProver #ITP #Math
October 5, 2026 at 12:11 PM
jalonso.eurosky.social
Soluciones del reto 21 de Lean 4: Las subsucesiones tienen el mismo límite que la sucesión. jaalonso.github.io/calculemus/p...

#RetoLean4 #LeanProver #ITP #Math
October 5, 2026 at 11:59 AM
jalonso.eurosky.social
Enunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. jaalonso.github.io/calculemus/p... #RetoLean4

#LeanProver #ITP #Math
October 5, 2026 at 12:15 PM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 17 (Las sucesiones convergentes están acotadas). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math
September 30, 2026 at 5:53 PM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 20 (Si aₙ → L y M es una cota superior de aₙ, entonces L ≤ M). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math
September 28, 2026 at 3:52 PM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 21 (Las subsucesiones tienen el mismo límite que la sucesión). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math
September 28, 2026 at 2:49 PM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 19 (Las sucesiones convergentes son de Cauchy). t.me/Retos_Matema... #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El Reto 19 consiste en demostrar, en Lean 4, que las sucesiones convergentes son de Cauchy. Para ello, hay que completar la siguiente teoría import Mathlib.Data.Real.Basic import Mathlib.Tactic vari...
t.me
September 17, 2026 at 3:22 PM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 18 (Convergencia del producto de sucesiones convergentes). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math
Reto 18: Convergencia del producto de sucesiones convergentes
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
jaalonso.github.io
September 17, 2026 at 3:21 PM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 16 (para todo n ∈ N, n(n+1)(2n+1) es divisible por 6). live.lean-lang.org#url=https://... #LeanProver #ITP #Math
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
live.lean-lang.org
August 30, 2026 at 10:40 AM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 17 (las sucesiones convergentes están acotadas). t.me/Retos_Matema... #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El Reto 17 consiste en demostrar, en Lean 4, las sucesiones convergentes están acotadas; es decir, que si existe un L ∈ ℝ tal que L es el límite de la sucesión aₙ es convergente, entonces existe un M ...
t.me
August 30, 2026 at 10:41 AM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 15 ((∃ k ∈ ℕ)(∀ n ∈ N)[(n + k)² ≤ 2ⁿ⁺ᵏ]). live.lean-lang.org#url=https://... #LeanProver #ITP #Math
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
live.lean-lang.org
August 24, 2026 at 3:48 PM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 16 (para todo n ∈ N, n(n+1)(2n+1) es divisible por 6). t.me/Retos_Matema... #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El Reto 16 consiste en demostrar, en Lean 4, que para todo n ∈ N, n(n+1)(2n+1) es divisible por 6. Para ello, hay que completar la siguiente teoría import Mathlib.Tactic variable (n : ℕ) example :...
t.me
August 24, 2026 at 3:49 PM
jalonso.eurosky.social
#Retolean4: Vídeo tutorial sobre cómo resolver el reto 14. youtu.be/ZWtaXZSXLko #LeanProver #ITP #Math
Reto 14 de Lean 4: 2n + 9 ≤ 2ⁿ⁺⁴
YouTube video by José A. Alonso
youtu.be
August 19, 2026 at 5:22 PM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). live.lean-lang.org#url=https://... #LeanProver #ITP #Math
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
live.lean-lang.org
August 19, 2026 at 5:21 PM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 15 ((∃ k ∈ ℕ)(∀ n ∈ N)[(n + k)² ≤ 2ⁿ⁺ᵏ]). t.me/Retos_Matema... #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El Reto 15 consiste en demostrar, en Lean 4, que (∃ k ∈ ℕ)(∀ n ∈ N)[(n + k)² ≤ 2ⁿ⁺ᵏ] Para ello, completa la siguiente teoría import Mathlib.Tactic example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n...
t.me
August 19, 2026 at 5:23 PM
jalonso.eurosky.social
#Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. youtu.be/EcNgDxgNya8 #LeanProver #ITP #Math
Reto 13 de Lean 4: Desigualdad triangular inversa
YouTube video by José A. Alonso
youtu.be
August 9, 2026 at 10:53 AM
jalonso.eurosky.social
#RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). live.lean-lang.org#url=https://... #LeanProver #ITP #Math
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
live.lean-lang.org
August 9, 2026 at 10:53 AM
jalonso.eurosky.social
#RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). t.me/Retos_Matema... #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El reto de esta semana consiste en demostrar, en Lean 4, que para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴ Para ello, completa la siguiente teoría import Mathlib.Tactic variable (n : ℕ) example : 2 * n + 9 ≤ 2 ^...
t.me
August 9, 2026 at 10:54 AM