José A. Alonso
@jalonso.bsky.social
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving.
Homepage: https://jaalonso.github.io
Sevilla, Spain
Homepage: https://jaalonso.github.io
Sevilla, Spain
Propositional logic proofs using Lean 4. ~ Kaue Silveira. kaue.me/wealth/caree... #ITP #LeanProver #Logic #Math
Propositional Logic Proofs Using Lean 4 - Kaue's Way of Life
This post provides a technical walkthrough of fundamental propositional logic concepts and their formal implementation using the Lean 4 programming language and theorem prover. It serves as a practica...
kaue.me
February 4, 2026 at 12:56 PM
Propositional logic proofs using Lean 4. ~ Kaue Silveira. kaue.me/wealth/caree... #ITP #LeanProver #Logic #Math
The evolution of a Lean programmer. unnamed.website/posts/evolut... #ITP #LeanProver #FunctionalProgramming
The Evolution of a Lean Programmer
Various implementations and proofs of insertion sort in Lean
unnamed.website
February 4, 2026 at 12:27 PM
The evolution of a Lean programmer. unnamed.website/posts/evolut... #ITP #LeanProver #FunctionalProgramming
Hello, Haskell: Getting started in 2026. ~ Lukasz Tymoszczuk. lukastymo.com/posts/025-he... #Haskell #FunctionalProgramming
Hello, Haskell: Getting Started in 2026
Read this if you want to:
see beginner examples that link Haskell’s syntax to its underlying mental models – types, pattern matching, declarative style and do see examples of Haskell’s distinctive syn...
lukastymo.com
February 4, 2026 at 11:54 AM
Hello, Haskell: Getting started in 2026. ~ Lukasz Tymoszczuk. lukastymo.com/posts/025-he... #Haskell #FunctionalProgramming
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory. ~ Tom de Jong, Nicolai Kraus, Axel Ljungström. arxiv.org/abs/2601.218... #ITP #Agda
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We sho...
arxiv.org
February 4, 2026 at 11:35 AM
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory. ~ Tom de Jong, Nicolai Kraus, Axel Ljungström. arxiv.org/abs/2601.218... #ITP #Agda
Formalization of non-Archimedean functional analysis 1: spherically complete spaces. ~ Yijun Yuan. arxiv.org/abs/2601.217... #ITP #LeanProver #Math
Formalization of non-Archimedean functional analysis 1: spherically complete spaces
In this article, we present a formalization of spherically complete spaces, which is a fundamental notion in non-archimedean functional analysis. This work includes the equivalent definitions of spher...
arxiv.org
February 4, 2026 at 11:35 AM
Formalization of non-Archimedean functional analysis 1: spherically complete spaces. ~ Yijun Yuan. arxiv.org/abs/2601.217... #ITP #LeanProver #Math
'Sets' revisited: Working with a large category in Isabelle/HOL. ~ Eugene W. Stark. www.isa-afp.org/entries/Sets... #ITP #IsabelleHOL
'Sets' Revisited: Working with a Large Category in Isabelle/HOL
'Sets' Revisited: Working with a Large Category in Isabelle/HOL in the Archive of Formal Proofs
www.isa-afp.org
February 4, 2026 at 11:34 AM
'Sets' revisited: Working with a large category in Isabelle/HOL. ~ Eugene W. Stark. www.isa-afp.org/entries/Sets... #ITP #IsabelleHOL
Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. ~ Tony Feng et als. arxiv.org/abs/2601.224... #AI4Math #ITP #LeanProver
Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems
We present a case study in semi-autonomous mathematics discovery, using Gemini to systematically evaluate 700 conjectures labeled 'Open' in Bloom's Erdős Problems database. We employ a hybrid methodol...
arxiv.org
February 4, 2026 at 11:34 AM
Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. ~ Tony Feng et als. arxiv.org/abs/2601.224... #AI4Math #ITP #LeanProver
Recent advances in LLMs for mathematics. ~ Sebastien Bubeck. youtu.be/MH3lG7V7SuU #AI4Math
Recent Advances in LLMs for Mathematics
YouTube video by Sebastien Bubeck
youtu.be
February 4, 2026 at 11:33 AM
Recent advances in LLMs for mathematics. ~ Sebastien Bubeck. youtu.be/MH3lG7V7SuU #AI4Math
Principles of programming languages. ~ Kristopher Micinski. kmicinski.com//cis352-s26/... #Programming #RacketLang
February 4, 2026 at 11:33 AM
Principles of programming languages. ~ Kristopher Micinski. kmicinski.com//cis352-s26/... #Programming #RacketLang
Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. arxiv.org/abs/2602.02091 #ITP #CoqProver
Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This problem was formula...
arxiv.org
February 4, 2026 at 11:33 AM
Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. arxiv.org/abs/2602.02091 #ITP #CoqProver
LeanArchitect: Automating blueprint generation for humans and AI. ~ Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck. arxiv.org/abs/2601.225... #AI4Math #ITP #LeanProver
LeanArchitect: Automating Blueprint Generation for Humans and AI
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human colla...
arxiv.org
February 4, 2026 at 11:32 AM
LeanArchitect: Automating blueprint generation for humans and AI. ~ Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck. arxiv.org/abs/2601.225... #AI4Math #ITP #LeanProver
Irrationality of rapidly converging series: a problem of Erdős and Graham. ~ Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, Shengtong Zhang. arxiv.org/abs/2601.21442 #AI4Math
Irrationality of rapidly converging series: a problem of Erdős and Graham
Answering a question of Erdős and Graham, we show that the double exponential growth condition $\limsup_{n\to\infty}a_n^{1/ϕ^n}=\infty$ for a strictly increasing sequence of positive integers $\{a_n\}...
arxiv.org
February 4, 2026 at 11:32 AM
Irrationality of rapidly converging series: a problem of Erdős and Graham. ~ Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, Shengtong Zhang. arxiv.org/abs/2601.21442 #AI4Math
Flow-based extremal mathematical structure discovery. ~ Gergely Bérczi, Baran Hashemi, Jonas Klüver. arxiv.org/abs/2601.180... #AI4Math
Flow-based Extremal Mathematical Structure Discovery
The discovery of extremal structures in mathematics requires navigating vast and nonconvex landscapes where analytical methods offer little guidance and brute-force search becomes intractable. We intr...
arxiv.org
February 4, 2026 at 11:31 AM
Flow-based extremal mathematical structure discovery. ~ Gergely Bérczi, Baran Hashemi, Jonas Klüver. arxiv.org/abs/2601.180... #AI4Math
Construction-verification: A benchmark for applied mathematics in Lean 4. ~ Bowen Yang et als. arxiv.org/abs/2602.012... #AI4Math #ITP #LeanProver
Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions...
arxiv.org
February 4, 2026 at 11:31 AM
Construction-verification: A benchmark for applied mathematics in Lean 4. ~ Bowen Yang et als. arxiv.org/abs/2602.012... #AI4Math #ITP #LeanProver
Calling Lean functions as Python functions. ~ Philip Zucker. www.philipzucker.com/leancall/ #ITP #LeanProver #Python
Calling Lean Functions As Python Functions
I think Lean is neat.
www.philipzucker.com
February 4, 2026 at 11:31 AM
Calling Lean functions as Python functions. ~ Philip Zucker. www.philipzucker.com/leancall/ #ITP #LeanProver #Python
A conversation on the future of mathematics. ~ Emily Riehl, Jesse Han, Jared Duker Lichtman. youtu.be/AJfoqKDenpw #ITP #LeanProver #Math
Emily Riehl — The future of mathematics | Math, Inc.
YouTube video by Math Inc
youtu.be
February 4, 2026 at 11:30 AM
A conversation on the future of mathematics. ~ Emily Riehl, Jesse Han, Jared Duker Lichtman. youtu.be/AJfoqKDenpw #ITP #LeanProver #Math
"Five-Point Haskell": Total depravity (and defensive typing). ~ Justin Le. blog.jle.im/entry/five-p... #Haskell #FunctionalProgramming
"Five-Point Haskell": Total Depravity (and Defensive Typing)
I have thought about distilling the principles by which I program Haskell, and how I’ve been able to steer long-lived projects over years of growth, refactorings, and changes in demands. I find myself...
blog.jle.im
February 4, 2026 at 11:30 AM
"Five-Point Haskell": Total depravity (and defensive typing). ~ Justin Le. blog.jle.im/entry/five-p... #Haskell #FunctionalProgramming
"Un paisaje es un estado del alma." ~ Henri-Frédéric Amiel (1821-1881).
February 4, 2026 at 8:08 AM
"Un paisaje es un estado del alma." ~ Henri-Frédéric Amiel (1821-1881).
#Exercitium: Diagonales principales de una matriz. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
February 3, 2026 at 7:01 PM
#Exercitium: Diagonales principales de una matriz. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
"La ironía es la agudeza que libera al espíritu." ~ Søren Kierkegaard (1813-1855).
February 3, 2026 at 12:59 PM
"La ironía es la agudeza que libera al espíritu." ~ Søren Kierkegaard (1813-1855).
#Exercitium: Segmentos de longitud dada. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming
February 2, 2026 at 11:57 AM
#Exercitium: Segmentos de longitud dada. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming
"La libre elección de amos no suprime ni a los amos ni a los esclavos." ~ Herbert Marcuse (1898-1979).
February 2, 2026 at 8:35 AM
"La libre elección de amos no suprime ni a los amos ni a los esclavos." ~ Herbert Marcuse (1898-1979).
#Exercitium: Reconocimiento de potencias de 2. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
February 1, 2026 at 1:42 PM
#Exercitium: Reconocimiento de potencias de 2. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
"La vida solo puede ser comprendida hacia atrás, pero debe ser vivida hacia adelante." ~ Søren Kierkegaard (1813-1855).
February 1, 2026 at 8:08 AM
"La vida solo puede ser comprendida hacia atrás, pero debe ser vivida hacia adelante." ~ Søren Kierkegaard (1813-1855).