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
"La humanidad tiene una moral doble: una que predica y no practica, y otra que practica y no predica." ~ Bertrand Russell (1872-1970).
January 5, 2026 at 7:17 AM
"La humanidad tiene una moral doble: una que predica y no practica, y otra que practica y no predica." ~ Bertrand Russell (1872-1970).
Readings shared January 03, 2026. jaalonso.github.io/vestigium/po... #AI #Emacs #ITP #LeanProver #Lisp #Math
Readings shared January 4, 2026
The readings shared in Bluesky on 4 January 2026 are:
Terry Tao on the future of mathematics. #AI #Math #ITP #LeanProver
Seemingly impossible programs in Lean. ~ Joachim Breitner. #ITP #LeanProver
Pu
jaalonso.github.io
January 5, 2026 at 7:16 AM
Readings shared January 03, 2026. jaalonso.github.io/vestigium/po... #AI #Emacs #ITP #LeanProver #Lisp #Math
Pursuit of truth and beauty in Lean 4 (Formally verified theory of grammars, optimization, matroids). ~ Martin Dvořák. madvorak.github.io/2026_Dvorak_... #ITP #LeanProver
January 4, 2026 at 10:34 AM
Pursuit of truth and beauty in Lean 4 (Formally verified theory of grammars, optimization, matroids). ~ Martin Dvořák. madvorak.github.io/2026_Dvorak_... #ITP #LeanProver
Emacs Lisp Elements: EPUB and PDF versions now available. ~ Protesilaos Stavrou. protesilaos.com/codelog/2025... #Emacs #Lisp
Emacs Lisp Elements: EPUB and PDF versions now available
My free book on the Emacs Lisp programming language is now available in EPUB and PDF formats.
protesilaos.com
January 4, 2026 at 8:30 AM
Emacs Lisp Elements: EPUB and PDF versions now available. ~ Protesilaos Stavrou. protesilaos.com/codelog/2025... #Emacs #Lisp
Terry Tao on the future of mathematics | Math, Inc.
YouTube video by Math Inc
youtu.be
January 4, 2026 at 8:04 AM
Seemingly impossible programs in Lean. ~ Joachim Breitner. www.joachim-breitner.de/blog/818-See... #ITP #LeanProver
January 4, 2026 at 8:00 AM
Seemingly impossible programs in Lean. ~ Joachim Breitner. www.joachim-breitner.de/blog/818-See... #ITP #LeanProver
An introduction to proofs and the mathematical vernacular. ~ Martin Day. personal.math.vt.edu/day/ProofsBo... #Math
January 4, 2026 at 7:44 AM
An introduction to proofs and the mathematical vernacular. ~ Martin Day. personal.math.vt.edu/day/ProofsBo... #Math
Open textbook library: Mathematics textbooks. open.umn.edu/opentextbook... #Math
January 4, 2026 at 7:41 AM
Open textbook library: Mathematics textbooks. open.umn.edu/opentextbook... #Math
Open textbook initiative (The American Institute of Mathematics (AIM)). textbooks.aimath.org #Math
January 4, 2026 at 7:38 AM
Open textbook initiative (The American Institute of Mathematics (AIM)). textbooks.aimath.org #Math
Computing and formalizing residuated lattices and relation algebras. ~ Peter Jipsen. jipsen.github.io/slides/Jipse... #ITP #LeanProver
January 4, 2026 at 7:32 AM
Computing and formalizing residuated lattices and relation algebras. ~ Peter Jipsen. jipsen.github.io/slides/Jipse... #ITP #LeanProver
Lecture Notes: Computational mathematics and AI (A ten-lecture workshop series). ~ Lars Ruthotto. www.cbmsweb.org/wp-content/u... #AI #Math
January 4, 2026 at 7:23 AM
Lecture Notes: Computational mathematics and AI (A ten-lecture workshop series). ~ Lars Ruthotto. www.cbmsweb.org/wp-content/u... #AI #Math
cLean: A verified domain-specific language for GPU kernel programming in Lean 4. ~ Riyaz Ahuja. riyazahuja.com/assets/clean... #ITP #LeanProver
January 4, 2026 at 7:03 AM
cLean: A verified domain-specific language for GPU kernel programming in Lean 4. ~ Riyaz Ahuja. riyazahuja.com/assets/clean... #ITP #LeanProver
"La felicidad se alcanza cuando lo que uno piensa, lo que uno dice y lo que uno hace están en armonía." ~ Mahatma Gandhi (1869-1948).
January 4, 2026 at 6:47 AM
"La felicidad se alcanza cuando lo que uno piensa, lo que uno dice y lo que uno hace están en armonía." ~ Mahatma Gandhi (1869-1948).
#Exercitium: Suma de una lista de vectores. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
January 3, 2026 at 6:41 PM
#Exercitium: Suma de una lista de vectores. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
"La cosa más difícil es conocernos a nosotros mismos; la más fácil es hablar mal de los demás."~ Tales de Mileto (aprox. 624-546 a.C.).
January 3, 2026 at 6:41 AM
"La cosa más difícil es conocernos a nosotros mismos; la más fácil es hablar mal de los demás."~ Tales de Mileto (aprox. 624-546 a.C.).
#Exercitium: Ordenación según una función. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
January 2, 2026 at 6:06 PM
#Exercitium: Ordenación según una función. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
"En cada invierno del corazón hay una trémula primavera, y tras el velo de cada noche se esconde un sonriente amanecer." ~ Khalil Gibran (1883-1931).
January 2, 2026 at 7:10 AM
"En cada invierno del corazón hay una trémula primavera, y tras el velo de cada noche se esconde un sonriente amanecer." ~ Khalil Gibran (1883-1931).
#Exercitium: Mezcla de infinitas listas infinitas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
January 1, 2026 at 12:15 PM
#Exercitium: Mezcla de infinitas listas infinitas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
Reposted by José A. Alonso
¿Qué mejor manera de esperar el comienzo de 2026 leyendo algunas curiosidades numéricas sobre ese número? Aquí te he dejado un buen puñado de ellas. ¡¡Feliz Año Feliz 2026!! 🤗🤗🤗
www.gaussianos.com/felices-fies...
www.gaussianos.com/felices-fies...
¡¡Felices Fiestas y Año Feliz 2026!! - Gaussianos
A menos de 24 horas del final de 2025, desde Gaussianos espero que hayáis tenido unas muy Felices Fiestas y que el 2026 que entrará muy pronto sea para
www.gaussianos.com
December 31, 2025 at 5:52 PM
¿Qué mejor manera de esperar el comienzo de 2026 leyendo algunas curiosidades numéricas sobre ese número? Aquí te he dejado un buen puñado de ellas. ¡¡Feliz Año Feliz 2026!! 🤗🤗🤗
www.gaussianos.com/felices-fies...
www.gaussianos.com/felices-fies...
"Hay que apartar de nosotros el mal gusto de querer coincidir con muchos." ~ Friedrich Nietzsche (1844-1900).
January 1, 2026 at 7:43 AM
"Hay que apartar de nosotros el mal gusto de querer coincidir con muchos." ~ Friedrich Nietzsche (1844-1900).
#Exercitium: Conjuntos de puntos enteros en regiones rectangulares. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
December 31, 2025 at 9:47 AM
#Exercitium: Conjuntos de puntos enteros en regiones rectangulares. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
"Se necesita toda la vida para aprender a vivir." ~ Lucio Anneo Séneca (-4, 65).
December 31, 2025 at 7:00 AM
"Se necesita toda la vida para aprender a vivir." ~ Lucio Anneo Séneca (-4, 65).
#Exercitium: Máxima suma de los segmentos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
December 30, 2025 at 11:11 AM
#Exercitium: Máxima suma de los segmentos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
"Exígete mucho a ti mismo y espera poco de los demás. Así te ahorrarás disgustos." ~ Confucio (-551, -479).
December 30, 2025 at 7:37 AM
"Exígete mucho a ti mismo y espera poco de los demás. Así te ahorrarás disgustos." ~ Confucio (-551, -479).
Readings shared December 29, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT
Readings shared December 29, 2025
The readings shared in Bluesky on 29 December 2025 are:
Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT
The biggest controversy in maths coul
jaalonso.github.io
December 30, 2025 at 7:37 AM
Readings shared December 29, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT