#Lean4Challenge
LightNews LightNews
jalonso.eurosky.social
Lean 4 challenge 25 solutions: If the interleaving of two sequences converges to L, then both converge to L.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
November 2, 2026 at 11:08 AM
jalonso.eurosky.social
Lean 4 challenge 14: For all n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
November 1, 2026 at 9:35 AM
jalonso.eurosky.social
Lean 4 challenge 16: For every n ∈ N, n(n+1)(2n+1) is divisible by 6.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
November 4, 2026 at 7:51 AM
jalonso.eurosky.social
Lean 4 challenge 13: Reverse triangle inequality: ||x| - |y|| ≤ |x - y|.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 31, 2026 at 7:49 AM
jalonso.eurosky.social
Lean 4 challenge 15: There exists k ∈ ℕ such that, for all n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
November 3, 2026 at 9:54 AM
jalonso.eurosky.social
Lean 4 challenge 26: Product of a sequence with limit zero and a bounded sequence.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
November 2, 2026 at 11:10 AM
jalonso.eurosky.social
Lean 4 challenge 12: If aₙ → L, bₙ → M and L < M, then eventually aₙ < bₙ.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 30, 2026 at 7:21 AM
jalonso.eurosky.social
Lean 4 challenge 11: If aₙ converges to L, then |aₙ| converges to |L|.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 29, 2026 at 10:27 AM
jalonso.eurosky.social
Lean 4 challenge 8 solutions: uniqueness of the limit. Also in Spanish on the blog.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 27, 2026 at 9:14 AM
jalonso.eurosky.social
Weekly reads: Oct 26 – Nov 1, 2026. Also in Spanish on the blog.

jaalonso.github.io/vestigium/en...

#AI #AI4Math #Autoformalization #IsabelleHOL #ITP #Lean4Challenge #LeanProver #Logic #Math
Weekly reads: Oct 26 – Nov 1, 2026
Here are the 27 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, now with two community reports: "The mathematical science
jaalonso.github.io
November 2, 2026 at 8:07 AM
jalonso.eurosky.social
Lean 4 challenge 10 solutions: If aₙ → L with L ≠ 0, then |aₙ| ≥ |L|/2 eventually.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 28, 2026 at 10:21 AM
jalonso.eurosky.social
Lean 4 challenge 24 solutions: the sequence 1, -1, 1, -1,... is not convergent. Also in Spanish on the blog.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 26, 2026 at 10:53 AM
jalonso.eurosky.social
Lean 4 challenge 25: If the interleaving of two sequences converges to L, then both converge to L. Also in Spanish on the blog.

jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 26, 2026 at 11:02 AM
jalonso.eurosky.social
Lean 4 challenge 7: The composition of injective functions is injective. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 25, 2026 at 8:00 AM
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
Lean 4 challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 24, 2026 at 7:37 AM
jalonso.eurosky.social
Lean 4 challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 23, 2026 at 9:42 AM
jalonso.eurosky.social
Lean 4 challenge 3: If aₙ converges to L, then 2aₙ converges to 2L. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 21, 2026 at 10:32 AM
jalonso.eurosky.social
Lean 4 challenge 24: The sequence 1, -1, 1, -1,... is not convergent (using Challenge 22). jaalonso.github.io/calculemus/e...

#Lean4Challenge #LeanProver #ITP #Math
October 19, 2026 at 3:09 PM
jalonso.eurosky.social
Solutions to Lean 4 challenge 23: The constant sequence aₙ = L converges to L. jaalonso.github.io/calculemus/e...

#Lean4Challenge #LeanProver #ITP #Math
October 19, 2026 at 3:03 PM
jalonso.eurosky.social
Challenge 2: The sequence 1, -1, 1, -1,... is not convergent. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 18, 2026 at 7:05 AM
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
Challenge 2: The sequence 1, -1, 1, -1,... is not convergent. jaalonso.github.io/calculemus/e... #LeanProver #ITP #Math #Lean4Challenge
October 18, 2026 at 7:04 AM
jalonso.eurosky.social
Challenge 1: Prove in Lean 4 that the sequence 1/n converges to 0. jaalonso.github.io/calculemus/e...

#LeanProver #ITP #Math #Lean4Challenge
October 16, 2026 at 8:51 AM