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
#Exercitium: Llanuras de longitud dada. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional
November 27, 2025 at 4:54 PM
#Exercitium: Llanuras de longitud dada. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional
An introduction to formal real analysis (Lecture 22: Uniformity). ~ Alex Kontorovich. youtu.be/VcYzMRJsA4Y #ITP #LeanProver #Math
Lecture 22, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 11/26/2025
YouTube video by Alex Kontorovich
youtu.be
November 27, 2025 at 10:17 AM
An introduction to formal real analysis (Lecture 22: Uniformity). ~ Alex Kontorovich. youtu.be/VcYzMRJsA4Y #ITP #LeanProver #Math
#MULCIA: PhD positions in automated and foundational verification at the Institute of Science and Technology Austria (ISTA). is.gd/VbhEov #PhD #CompSci
November 27, 2025 at 10:01 AM
#MULCIA: PhD positions in automated and foundational verification at the Institute of Science and Technology Austria (ISTA). is.gd/VbhEov #PhD #CompSci
"El hombre actual ha nacido o bien para vivir entre las convulsiones de la inquietud, o bien en el letargo del aburrimiento." ~ Voltaire (1694-1778).
November 27, 2025 at 9:51 AM
"El hombre actual ha nacido o bien para vivir entre las convulsiones de la inquietud, o bien en el letargo del aburrimiento." ~ Voltaire (1694-1778).
Readings shared November 26, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #Math #TypeTheory
Readings shared November 26, 2025
The readings shared in Bluesky on 26 November 2025 are:
Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. #ITP #IsabelleHOL #Math
Introduc
jaalonso.github.io
November 27, 2025 at 9:50 AM
Readings shared November 26, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #Math #TypeTheory
Reposted by José A. Alonso
#Exercitium: Expresiones vectoriales. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
Expresiones vectoriales
El siguiente tipo de dato define las expresiones vectoriales formadas por un vector, la suma de dos expresiones vectoriales o el producto de un entero por una expresión vectorial.
data ExpV = Vec Int
jaalonso.github.io
November 26, 2025 at 5:57 PM
#Exercitium: Expresiones vectoriales. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. arxiv.org/abs/2511.20550 #ITP #IsabelleHOL #Math
Verifying Numerical Methods with Isabelle/HOL
Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. Therefore, we contr...
arxiv.org
November 26, 2025 at 10:43 AM
Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. arxiv.org/abs/2511.20550 #ITP #IsabelleHOL #Math
Lambda calculus and typing. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming #LambdaCalculus #TypeTheory
November 26, 2025 at 10:37 AM
Lambda calculus and typing. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming #LambdaCalculus #TypeTheory
Higher-order functions and type classes. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
November 26, 2025 at 10:35 AM
Higher-order functions and type classes. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
First-order data types and pattern-matching ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
November 26, 2025 at 10:33 AM
First-order data types and pattern-matching ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
Introduction to functional programming. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
November 26, 2025 at 10:32 AM
Introduction to functional programming. ~ Noam Zeilberger. noamz.org/teaching/CSE... #Haskell #FunctionalProgramming
"Cuando te esfuerzas por no censurar a los demás, tu vida resulta mucho más fácil, pero muy poca gente lleva a cabo este pequeño esfuerzo." ~ León Tolstói (1828-1910).
November 26, 2025 at 10:25 AM
"Cuando te esfuerzas por no censurar a los demás, tu vida resulta mucho más fácil, pero muy poca gente lleva a cabo este pequeño esfuerzo." ~ León Tolstói (1828-1910).
Readings shared November 25, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Programming #Rocq
Readings shared November 25, 2025
The readings shared in Bluesky on 25 November 2025 are:
Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L
jaalonso.github.io
November 26, 2025 at 10:23 AM
Readings shared November 25, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Programming #Rocq
#Exercitium: Expresiones aritmética normalizadas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
November 25, 2025 at 5:10 PM
#Exercitium: Expresiones aritmética normalizadas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
Reposted by José A. Alonso
Just out: Functional Data Structures, edited by Tobias Nipkow
November 25, 2025 at 12:48 PM
Just out: Functional Data Structures, edited by Tobias Nipkow
Software never fails. ~ kqr. entropicthoughts.com/software-nev... #Programming
November 25, 2025 at 11:32 AM
Software never fails. ~ kqr. entropicthoughts.com/software-nev... #Programming
MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. arxiv.org/abs/2503.04763 #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs
MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language ...
arxiv.org
November 25, 2025 at 11:28 AM
MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. arxiv.org/abs/2503.04763 #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs
REAL-Prover: Retrieval augmented lean prover for mathematical reasoning. ~ Ziju Shen et als. arxiv.org/abs/2505.20613 #ITP #LeanProver #LLMs #Math
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL...
arxiv.org
November 25, 2025 at 11:24 AM
REAL-Prover: Retrieval augmented lean prover for mathematical reasoning. ~ Ziju Shen et als. arxiv.org/abs/2505.20613 #ITP #LeanProver #LLMs #Math
Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras. arxiv.org/abs/2511.19142 #ITP #LeanProver
Formalizing Computational Paths and Fundamental Groups in Lean
Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborators and yields a weak...
arxiv.org
November 25, 2025 at 11:20 AM
Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras. arxiv.org/abs/2511.19142 #ITP #LeanProver
"Cada uno toma los límites de su propia visión como los límites del mundo." ~ Arthur Schopenhauer (1788-1860).
November 25, 2025 at 11:09 AM
"Cada uno toma los límites de su propia visión como los límites del mundo." ~ Arthur Schopenhauer (1788-1860).
Readings shared November 24, 2025. jaalonso.github.io/vestigium/po... #CompSci #CoqProver #ITP #LeanProver #Logic #Math #Physics #SetTheory #TypeTheory
Readings shared November 24, 2025
The readings shared in Bluesky on 24 November 2025 are:
An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. #ITP #LeanProver #Math
A perspective on in
jaalonso.github.io
November 25, 2025 at 11:08 AM
Readings shared November 24, 2025. jaalonso.github.io/vestigium/po... #CompSci #CoqProver #ITP #LeanProver #Logic #Math #Physics #SetTheory #TypeTheory
A new bridge links the strange math of infinity to computer science. ~ Joseph Howlett. www.quantamagazine.org/a-new-bridge... #Math #CompSci
A New Bridge Links the Strange Math of Infinity to Computer Science | Quanta Magazine
Descriptive set theorists study the niche mathematics of infinity. Now, they’ve shown that their problems can be rewritten in the concrete language of algorithms.
www.quantamagazine.org
November 24, 2025 at 6:56 PM
A new bridge links the strange math of infinity to computer science. ~ Joseph Howlett. www.quantamagazine.org/a-new-bridge... #Math #CompSci
Automatic geometry theorem proving using polynomial elaboration. ~ Mauricio Barba da Costa et als. youtu.be/1FjQzA8S7Z4 #ITP #LeanProver #Math
Automatic Geometry Theorem Proving Using Polynomial Elaboration | Mauricio Barba da Costa
YouTube video by Icelandic Centre of Excellence in Theoretical CS
youtu.be
November 24, 2025 at 6:49 PM
Automatic geometry theorem proving using polynomial elaboration. ~ Mauricio Barba da Costa et als. youtu.be/1FjQzA8S7Z4 #ITP #LeanProver #Math