banner
LightNews
jalonso.bsky.social
José A. Alonso
@jalonso.bsky.social
1.7K followers 660 following 4.9K posts
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving. Homepage: https://jaalonso.github.io Sevilla, Spain
jaalonso.github.io
Posts Media Videos Starter Packs
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 14h
"La verdadera felicidad consiste en no hacer nada en particular, en no tener que ir a ninguna parte, en no tener que ser nadie." ~ Lin Yutang (1895-1975).
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 14h
Readings shared October 11, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math
Readings shared October 11, 2025
The readings shared in Bluesky on 11 October 2025 are: An introduction to formal real analysis (Lecture 9: Finite sums and boundedness of convergent sequences). ~ Alex Kontorovich. #ITP #LeanProver #
jaalonso.github.io
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
#Exercitium: Laberinto numérico. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
An introduction to formal real analysis (Lecture 10: Algebraic limit theorem and order properties). ~ Alex Kontorovich. youtu.be/eX3Z8wzuINM #ITP #LeanProver #Math
Lecture 10, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 10/10/2025
YouTube video by Alex Kontorovich
youtu.be
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
An introduction to formal real analysis (Lecture 9: Finite sums and boundedness of convergent sequences). ~ Alex Kontorovich. youtu.be/oXTSs3GtkB0 #ITP #LeanProver #Math
Lecture 9, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 10/07/2025
YouTube video by Alex Kontorovich
youtu.be
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
"La sabiduría de vivir consiste en eliminar lo que no es indispensable." ~ Lin Yutang (1895-1975).
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
Readings shared October 10, 2025. jaalonso.github.io/vestigium/po... #AI #CoqProver #Dafny #FormalMethods #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Programming
Readings shared October 9, 2025
The readings shared in Bluesky on 9 October 2025 are: State management in Haskell. ~ Ajeet Grewal. #Haskell #FunctionalProgramming Haskell is the perfect fit for renewable energy tech. ~ Marc Jakobi.
jaalonso.github.io
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
#Exercitium: Sustitución en una expresión aritmética. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Relational divisibility (in Isabelle/HOL). ~ Walter Guttmann. www.isa-afp.org/entries/Rela... #ITP #IsabelleHOL #Math
Relational Divisibility
Relational Divisibility in the Archive of Formal Proofs
www.isa-afp.org
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Mathematicians’ new best friend? ~ Benjamin Skuse. scilogs.spektrum.de/hlf/mathemat... #AI #Math
Mathematicians’ New Best Friend?
A recent blog post highlighted three Spark Session talks at the 12th Heidelberg Laureate Forum that focused on the potential for a new era of superhuman AI capabilities through AI self-improvement and...
scilogs.spektrum.de
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Languages. Formal Systems. Inference rules. Proofs. ~ Andrei Arusoaie. edu.info.uaic.ro/metode-forma... #FormalMethods #Logic #Dafny
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Languages. Formal Systems. Inference rules. Proofs. ~ Andrei Arusoaie. edu.info.uaic.ro/metode-forma... #FormalMethods #Logic #Dafny
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Formal methods in software engineering. ~ Andrei Arusoaie. edu.info.uaic.ro/metode-forma... #FormalMethods
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Principles of programming languages: A little bit of history. ~ Andrei Arusoaie. edu.info.uaic.ro/principii-al... #Programming
5 5
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Principles of programming languages (lecture notes for CS2105O2). ~ Andrei Arusoaie. edu.info.uaic.ro/principii-al... #ITP #CoqProver
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
ADTs, functions and induction. ~ Andrei Arusoaie. edu.info.uaic.ro/principii-al... #ITP #LeanProver #FunctionalProgramming
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Markov kernels in Mathlib's probability library. ~ Rémy Degenne. arxiv.org/abs/2510.040... #ITP #LeanProver #Math
1 1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
"La realidad está definida con palabras. Por lo tanto, el que controla las palabras controla la realidad." ~ Antonio Gramsci (1891-1937).
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Readings shared October 9, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Math
Readings shared October 9, 2025
The readings shared in Bluesky on 9 October 2025 are: State management in Haskell. ~ Ajeet Grewal. #Haskell #FunctionalProgramming Haskell is the perfect fit for renewable energy tech. ~ Marc Jakobi.
jaalonso.github.io
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
Mathematics: The rise of the machines. ~ Yang-Hui He. youtu.be/oOYcPkBaotg #AI #Math #LLMs #ITP #LeanProver
Mathematics: The rise of the machines
YouTube video by The Royal Institution
youtu.be
3
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
Why Haskell is the perfect fit for renewable energy tech. ~ Marc Jakobi. mrcjkb.dev/posts/2025-1... #Haskell #FunctionalProgramming
2 5
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
State management in Haskell. ~ Ajeet Grewal. grewal.dev/posts/haskel... #Haskell #FunctionalProgramming
1 2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
#Exercitium: Clausura de un conjunto respecto de una función. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
"Así como no sentimos la salud de todo nuestro cuerpo sino solo el punto donde nos aprieta el zapato, tampoco pensamos en todos nuestros asuntos que marchan perfectamente bien sino en alguna pequeñez insignificante que nos disgusta." ~ Arthur Schopenhauer (1788-1860).
1 1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 3d
Readings shared October 8, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib
Readings shared October 8, 2025
The readings shared in Bluesky on 8 October 2025 are: Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Mic
jaalonso.github.io