#LeanProver
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 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 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
johnericson.me
I'm a little saddened that to casual observers, github.com/leanprover-c... and AI doing math are probably encountered as a singular highly disruptive event, when the former exists without the latter and is a marvel of modern librarianship.
GitHub - leanprover-community/mathlib4: The math library of Lean 4
The math library of Lean 4. Contribute to leanprover-community/mathlib4 development by creating an account on GitHub.
github.com
October 28, 2026 at 3:10 PM
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 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
Reasoning about the Genetic Code in Lean. ~ Colin T. Jones, Tyler R. Josephson.

arxiv.org/abs/2610.36343

#LeanProver #ITP
Reasoning about the Genetic Code in Lean
The genetic code exhibits redundancy, meaning that multiple distinct nucleotide sequences can encode the same amino acid sequence, a property mathematically characterized as non-injectivity. While thi...
arxiv.org
November 2, 2026 at 12:48 PM
jalonso.eurosky.social
Automatic certified differentiation in Lean. ~ Ramy Shahin.

arxiv.org/abs/2610.363...

#LeanProver #ITP #Math
Automatic Certified Differentiation in Lean
Automatic differentiation (the automatic computation of numerical function derivatives) has many applications, especially in scientific computing and machine learning. Several approaches to automate t...
arxiv.org
November 2, 2026 at 12:43 PM
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
Reasoning about the genetic code in Lean. ~ Colin T. Jones, Tyler R. Josephson.

arxiv.org/abs/2610.36343

#LeanProver #ITP
Reasoning about the Genetic Code in Lean
The genetic code exhibits redundancy, meaning that multiple distinct nucleotide sequences can encode the same amino acid sequence, a property mathematically characterized as non-injectivity. While thi...
arxiv.org
October 28, 2026 at 12:10 PM
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
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 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
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
KAPPA: Checking the proofs in statistics papers with Lean 4 and language model agents. ~ Zihua She, Xiao Wang.

arxiv.org/abs/2610.35596

#LeanProver #ITP #AI4Math
KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organ...
arxiv.org
November 2, 2026 at 12:57 PM
jalonso.eurosky.social
Algebraic completeness of Feynman premeasures: The Henstock-Kurzweil path integral and operator wick calculus in Lean 4. ~ Yu. N. Berdinsky.

arxiv.org/abs/2610.37346

#LeanProver #ITP #Math
Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
We formalize in Lean 4 the gauge closure of the Feynman functional integral for the free field without Wick rotation. First, the restriction to box divisions is removed via a direction bound and a uni...
arxiv.org
November 2, 2026 at 12:46 PM
jalonso.eurosky.social
Two-colour zig-zag numberlink on rectangles: a forbidden-pattern characterization, a constructive polynomial-time algorithm, and a Lean verification. ~ Zzyv Zzyzek.

arxiv.org/abs/2610.37691

#LeanProver #ITP
Two-Colour Zig-Zag Numberlink on Rectangles: A Forbidden-Pattern Characterization, a Constructive Polynomial-Time Algorithm, and a Lean Verification
In Zig-Zag Numberlink, pairs of endpoints in a grid must be joined by vertex-disjoint paths that together visit every cell. The problem is NP-complete when the number of pairs is un- bounded (Adcock e...
arxiv.org
November 2, 2026 at 12:50 PM
jalonso.eurosky.social
The classification of finite simple groups, formalized in Lean.

cfsg.axiommath.ai

#LeanProver #ITP #AI4Math #AI #Math
The Classification of Finite Simple Groups, formalized in Lean
A complete formalization in Lean of the first-generation proof of the classification of finite simple groups, with every logical step checked by Lean’s kernel.
cfsg.axiommath.ai
October 27, 2026 at 6:07 PM
jalonso.eurosky.social
Formalizing the Enormous Theorem (Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics).

axiommath.ai/research/the...

#LeanProver #ITP #AI4Math #AI #Math
Formalizing the Enormous Theorem
Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics.
axiommath.ai
October 27, 2026 at 5:00 PM
jalonso.eurosky.social
PaperFormalizer: Author-in-the-loop autoformalization of research papers in Lean. ~ Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet.

arxiv.org/abs/2610.31810

#LeanProver #ITP #AI4Math #Autoformalization
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps i...
arxiv.org
October 26, 2026 at 11:41 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
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