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
De la disputatio a la IA: regreso a los orígenes (La universidad como lugar de diálogo). ~ Neila Campos. www.universidadsi.es/de-la-disput... #AI #Education
De la disputatio a la IA: regreso a los orígenes - Universidad, sí
La llegada de la IA también reabre, de forma inesperada, la vieja cuestión del debate dialéctico. Si un estudiante puede escribir su trabajo con ayuda de una IA, el modelo de evaluación basado en la p...
www.universidadsi.es
November 11, 2025 at 1:02 PM
De la disputatio a la IA: regreso a los orígenes (La universidad como lugar de diálogo). ~ Neila Campos. www.universidadsi.es/de-la-disput... #AI #Education
Computer-assisted proofs in Lean4. ~ J. Nijholt. fse.studenttheses.ub.rug.nl/37126/1/bMAT... #ITP #LeanProver #Math
November 11, 2025 at 12:54 PM
Computer-assisted proofs in Lean4. ~ J. Nijholt. fse.studenttheses.ub.rug.nl/37126/1/bMAT... #ITP #LeanProver #Math
"No me arrepiento de nada. El que se arrepiente de lo que ha hecho es doblemente miserable." ~ Baruch Spinoza (1632-1677).
November 11, 2025 at 12:43 PM
"No me arrepiento de nada. El que se arrepiente de lo que ha hecho es doblemente miserable." ~ Baruch Spinoza (1632-1677).
Readings shared November 10, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #Math
Readings shared November 10, 2025
The readings shared in Bluesky on 10 November 2025 are:
Apriori knowledge in an era of computational opacity: The Role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math
#Exerciti
jaalonso.github.io
November 11, 2025 at 12:43 PM
Readings shared November 10, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #Math
Reposted by José A. Alonso
Around ten years ago Marijn Heule, Oliver Kullmann and Victor Marek proved that if you 2-colour the positive integers from 1 to 7825, then you must be able to find x, y and z all of the same colour with x^2+y^2=z^2 -- that is, a monochromatic Pythagorean triple. 1/
November 11, 2025 at 9:30 AM
Around ten years ago Marijn Heule, Oliver Kullmann and Victor Marek proved that if you 2-colour the positive integers from 1 to 7825, then you must be able to find x, y and z all of the same colour with x^2+y^2=z^2 -- that is, a monochromatic Pythagorean triple. 1/
#Exercitium: Mínimos locales. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
November 10, 2025 at 5:45 PM
#Exercitium: Mínimos locales. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
Apriori knowledge in an era of computational opacity: The Role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. www.cambridge.org/core/journal... #AI #Math
November 10, 2025 at 11:33 AM
Apriori knowledge in an era of computational opacity: The Role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. www.cambridge.org/core/journal... #AI #Math
"La imaginación es la mitad de la enfermedad, la tranquilidad es la mitad del remedio y la paciencia es el comienzo de la cura." ~ Avicena (980-1037).
November 10, 2025 at 11:27 AM
"La imaginación es la mitad de la enfermedad, la tranquilidad es la mitad del remedio y la paciencia es el comienzo de la cura." ~ Avicena (980-1037).
The philosophical prospects of Large Language Models in the future of mathematics. ~ Fenner Stanley Tanswell, Ásgeir Berg. philsci-archive.pitt.edu/27017/1/The%... #AI #Math
November 9, 2025 at 10:39 AM
The philosophical prospects of Large Language Models in the future of mathematics. ~ Fenner Stanley Tanswell, Ásgeir Berg. philsci-archive.pitt.edu/27017/1/The%... #AI #Math
Towards formalizing reinforcement learning theory. ~ Shangtong Zhang. arxiv.org/abs/2511.036... #ITP #LeanProver
Towards Formalizing Reinforcement Learning Theory
In this paper, we formalize the almost sure convergence of $Q$-learning and linear temporal difference (TD) learning with Markovian samples using the Lean 4 theorem prover based on the Mathlib library...
arxiv.org
November 9, 2025 at 10:35 AM
Towards formalizing reinforcement learning theory. ~ Shangtong Zhang. arxiv.org/abs/2511.036... #ITP #LeanProver
#MULCIA: Postdoc Position in AI Theorem Proving (ProofBench Project), TU Freiberg (Germany). tinyurl.com/29e3o7dh #PostDoc #CompSci #AI
November 9, 2025 at 10:21 AM
#MULCIA: Postdoc Position in AI Theorem Proving (ProofBench Project), TU Freiberg (Germany). tinyurl.com/29e3o7dh #PostDoc #CompSci #AI
"Hay quienes, obsesionados con la prudencia , por querer evitar hasta el más mínimo error, convierten toda su vida en un único error." ~ Arturo Graf (1948-1913).
November 9, 2025 at 10:13 AM
"Hay quienes, obsesionados con la prudencia , por querer evitar hasta el más mínimo error, convierten toda su vida en un único error." ~ Arturo Graf (1948-1913).
Readings shared November 8, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #FunctionalProgramming #Haskell #ITP #LeanProver #Math
Readings shared November 8, 2025
The readings shared in Bluesky on 8 November 2025 are:
A new paradigm for mathematical proof? ~ Emily Riehl. #AI #Math #ITP #Agda #LeanProver
An introduction to formal real analysis (Lecture 17: Seri
jaalonso.github.io
November 9, 2025 at 10:13 AM
Readings shared November 8, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #FunctionalProgramming #Haskell #ITP #LeanProver #Math
#Exercitium: Pequeño test de inteligencia. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
November 8, 2025 at 6:14 PM
#Exercitium: Pequeño test de inteligencia. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
An introduction to formal real analysis (Lecture 17: Series and convergence). ~ Alex Kontorovich. youtu.be/cTbVEisk0rI #ITP #LeanProver #Math
Lecture 17, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 11/07/2025
YouTube video by Alex Kontorovich
youtu.be
November 8, 2025 at 11:45 AM
An introduction to formal real analysis (Lecture 17: Series and convergence). ~ Alex Kontorovich. youtu.be/cTbVEisk0rI #ITP #LeanProver #Math
A new paradigm for mathematical proof? ~ Emily Riehl. youtu.be/fzxW2XJS6SE #AI #Math #ITP #Agda #LeanProver
Emily Riehl, A New Paradigm for Mathematical Proof? | Natural Philosophy Symposium 2025
YouTube video by Hopkins Natural Philosophy Forum
youtu.be
November 8, 2025 at 11:41 AM
A new paradigm for mathematical proof? ~ Emily Riehl. youtu.be/fzxW2XJS6SE #AI #Math #ITP #Agda #LeanProver
"El que en un arte ha llegado a maestro puede prescindir de las reglas." ~ Arturo Graf (1948-1913).
November 8, 2025 at 10:48 AM
"El que en un arte ha llegado a maestro puede prescindir de las reglas." ~ Arturo Graf (1948-1913).
#Exercitium: Mayores elementos de una matriz. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
November 7, 2025 at 7:28 PM
#Exercitium: Mayores elementos de una matriz. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
An introduction to formal real analysis (Lecture 16: Completeness of the real numbers). ~ Alex Kontorovich. youtu.be/omfZbs2v_dQ #ITP #LeanProver #Math
Lecture 16, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 11/4/2025
YouTube video by Alex Kontorovich
youtu.be
November 7, 2025 at 6:19 PM
An introduction to formal real analysis (Lecture 16: Completeness of the real numbers). ~ Alex Kontorovich. youtu.be/omfZbs2v_dQ #ITP #LeanProver #Math
The path to a superhuman AI mathematician. (Mathematics is the first place where evidence of AI superintelligence is likely to appear, a theoretical computer scientist says). ~ Lawrence Fisher. cacm.acm.org/news/the-pat... #AI #Math #ITP #LeanProver
November 7, 2025 at 1:12 PM
The path to a superhuman AI mathematician. (Mathematics is the first place where evidence of AI superintelligence is likely to appear, a theoretical computer scientist says). ~ Lawrence Fisher. cacm.acm.org/news/the-pat... #AI #Math #ITP #LeanProver
Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. arxiv.org/abs/2409.19176 #ITP #Agda #HoTT
Polynomial Universes in Homotopy Type Theory
Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. Their work presented ...
arxiv.org
November 7, 2025 at 12:29 PM
Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. arxiv.org/abs/2409.19176 #ITP #Agda #HoTT
Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. hal.science/hal-05342510... #ITP #LeanProver #Rocq
November 7, 2025 at 8:26 AM
Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. hal.science/hal-05342510... #ITP #LeanProver #Rocq
ScenicProver: A framework for compositional probabilistic verification of learning-enabled systems. ~ Eric Vin et als. arxiv.org/abs/2511.021... #ITP #LeanProver
ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either...
arxiv.org
November 7, 2025 at 8:21 AM
ScenicProver: A framework for compositional probabilistic verification of learning-enabled systems. ~ Eric Vin et als. arxiv.org/abs/2511.021... #ITP #LeanProver
Math reasoning in times of AI: Lean way of theorem proving. ~ Jan Cepika et als. home.zcu.cz/~danek/DATA/... #ITP #LeanProver #Math #AI #LLM
November 7, 2025 at 8:13 AM
Math reasoning in times of AI: Lean way of theorem proving. ~ Jan Cepika et als. home.zcu.cz/~danek/DATA/... #ITP #LeanProver #Math #AI #LLM