José A. Alonso
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving.
Homepage: https://jaalonso.github.io
Sevilla, Spain
- "Si alguien no marcha al mismo paso que sus compañeros, tal vez es que escucha un tambor distinto." ~ Henry David #Thoreau (1817-1862).
- Readings shared February 05, 2026. jaalonso.github.io/vestigium/po...
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- "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).
- #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).
- #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).
- #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).
- #Exercitium: Menor número triangular con más de n divisores. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
- "Los hombres se equivocan al creerse libres, opinión que obedece al solo hecho de que son conscientes de sus acciones e ignorantes de las causas que las determinan." ~ Baruch Spinoza (1632-1677).
- #Exercitium: Particiones de enteros positivos. jaalonso.github.io/exercitium/p... #Haskell #FunctionalProgramming #Math
- "El egoísmo no es vivir como uno desea vivir, es pedir a los demás que vivan como uno desea vivir. Y la generosidad consiste en dejar tranquila la vida de los demás, sin interferir en ella." ~ Oscar Wilde (1854-1900)
- Readings shared January 29, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #FunctionalProgramming #Hakell #ITP #IsabelleHOL #LLMs #LeanProver #Math
- Metaprogramming the next generation of testing tools. ~ Harry Goldstein. youtu.be/AFbnS9xuPhY #ITP #LeanProver
- What's new in the Lean standard library. ~ Markus Himmel, Sofia Rodrigues. youtu.be/Il8xUcO15pE #ITP #LeanProver
- Aristotle, an AI theorem prover using Lean. ~ Alex Best. youtu.be/XmD-Vl2iiqM #AI #Math #AI4Math #ITP #LeanProver #Aristotle
- Formal verification of Rust cryptographic code in Lean with Aeneas. ~ Son Ho. youtu.be/ZzDpWjeUNdI #ITP #LeanProver
- Internal projectivity of the sequence space in Lean. ~ Jonas van der Schaaf. youtu.be/CD_GplIChms #ITP #LeanProver #Math
- The sphere packing project. ~ Sidharth Hariharan, Seewoo Lee, Chris Birkbeck. youtu.be/mq0P9BMyGPQ #ITP #LeanProver
- Autoformalization for physics and engineering with Lean. ~ Leopoldo Sarra. youtu.be/avhErya_gCg #ITP #LeanProver
- Teaching real analysis as a video game. ~ Alex Kontorovich. youtu.be/gSDLLBPDiKQ #ITP #LeanProver #Math
- Verification of model-checking techniques in Lean. ~ Atticus Kuhn. youtu.be/UZzZrTR3o6I #ITP #LeanProver
- Hopf algebras, affine group schemes and all of that. ~ Yaël Dillies. youtu.be/cz9Q4TtveL0 #ITP #LeanProver #Math
