Mathematician interested in the study and teaching of computational logic, functional programming (Haskell) and interactive theorem proving (Lean, Isabelle/HOL).
Public Key
npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw Profile Code
nprofile1qqsqa7mmeyplf3n3dn2dq7ps6dzd02l9kcr6z4k78n0p4sd9hu32u8qpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dseqx3lp
Show more details
Published at
2026-07-16T11:57:19Z Event JSON
{
"id": "a79137c297e10af28c0d3b5b13e40d9479af4c4fd01c8608dfb463155a93f252" ,
"pubkey": "0efb7bc903f4c6716cd4d07830d344d7abe5b607a156de3cde1ac1a5bf22ae1c" ,
"created_at": 1784203039 ,
"kind": 0 ,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/Jose_A_Alonso",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "{\"name\":\"José A. Alonso\",\"about\":\"Mathematician interested in the study and teaching of computational logic, functional programming (Haskell) and interactive theorem proving (Lean, Isabelle/HOL).\",\"picture\":\"https://media.mathstodon.xyz/accounts/avatars/000/130/356/original/29218903abe161c6.jpg\",\"banner\":\"https://media.mathstodon.xyz/accounts/headers/000/130/356/original/5493106ed84056f5.png\",\"nip05\":\"[email protected] \",\"fields\":[[\"Website\",\"https://jaalonso.github.io/\"],[\"Twitter\",\"https://twitter.com/Jose_A_Alonso\"],[\"Blog\",\"https://www.glc.us.es/~jalonso/vestigium/\"],[\"GitHub\",\"https://github.com/jaalonso\"]]}" ,
"sig": "f7b8bc8c2988202985fb2738a929985b4c1563bbd3c2149255aaf4a8755e6d29a4862ac06961d56312c24ed803fcb936008cb8c1cbb1a6bce6818b931be889d3"
}
Last Notes npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso A Rocq-based formalization of Hilbert’s geometry: Building a reusable foundation for 3D perpendicularity theory and verification. ~ Qimeng Zhang, Wensheng Yu. https://www.mdpi.com/2297-8747/31/1/25 #RocqProver #ITP #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Accelerating mathematics. ~ Kevin Buzzard. https://xenaproject.wordpress.com/2026/02/09/accelerating-mathematics/ #AI4Math #ITP #LeanProver npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Es preciso que cambie a cada momento, porque dejar de transformarse es dejar de vivir." ~ Henri Bergson (1959-1941). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #MULCIA: Haskell software engineer for remote position at IOG (Input Output Global). https://tinyurl.com/23x85sha #Jobs #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared July 28, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/29-readings_shared_07-28-25 #FormalVerification #FunctionalProgramming #Haskell #LeanProver #Logic #Math #ProofAssistant npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.1.pdf #ATP #ITP #Mizar #Aga #IsabelleHOL #LeanProver #Coq #Rocq #Education npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Exercitium: Biparticiones de una lista. https://jaalonso.github.io/exercitium/posts/2014/05/23-biparticiones_de_una_lista/ #Haskell #ProgramaciónFuncional npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Calculemus: El problema de los infectados. https://jaalonso.github.io/calculemus/posts/2020/03/19-el_problema_de_los_infectados/ #IsabelleHOL #Lógica #Matemática npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Calculemus: La dama o el tigre. https://jaalonso.github.io/calculemus/posts/2020/03/12-la_dama_o_el_tigre #IsabelleHOL #Lógica npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #MULCIA: Post-doctoral fellow in formal verification of multi-agent systems. https://tinyurl.com/22ssea82 #PostDoc #CompSci npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Pensar es difícil. Por eso la mayoría de la gente prefiere juzgar." ~ Carl Gustav Jung (1875-1961). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Calculemus: El problema lógico del mal. https://jaalonso.github.io/calculemus/posts/2020/03/05-el_problema_logico_del_mal #ITP #IsabelleHOL #Lógica npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso The Haskell Unfolder Episode 40: Understanding through a model. ~ Edsko de Vries, Andres Löh. https://www.youtube.com/live/0QTt2W7CVnA #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Calculemus: Teorema de Nicómaco. https://jaalonso.github.io/calculemus/posts/2020/01/30-teorema_de_nicomaco/ #IsabelleHOL #Lógica #Matemática npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "He descubierto que toda la maldad humana proviene de la incapacidad del ser humano de sentarse en calma en una habitación." ~ Blaise Pascal (1623-1662). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Curso "Lógica informática (2004-05)". https://jaalonso.github.io/cursos/li-04 #Logic #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Navigating between points with registers. ~ Daniel Liden. https://www.danliden.com/notes/20250308-registers-1.html #Emacs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso DeepSeek vs. ChatGPT vs. Claude: A comparative study for scientific computing and scientific machine learning tasks. ~ Qile Jiang, Zhiwei Gao, George Em Karniadakis. https://arxiv.org/abs/2502.17764 #LLMs #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Calculemus: Celebración del día mundial de la lógica. https://jaalonso.github.io/calculemus/posts/2020/01/14-celebracion_del_dia_mundial_de_la_logica/ #IsabelleHOL #Lógica #Matemática npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso FANS: Formal answer selection for natural language math reasoning using Lean4. ~ Jiarui Yao, Ruida Wang, Tong Zhang. https://arxiv.org/abs/2503.03238 #LLMs #ITP #LeanProver npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared March 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/05-readings_shared_03-05-25 #ITP #IsabelleHOL #AI #Education npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Language partitioning for mission-time linear temporal logic (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian, Alec Rosentrater. https://www.isa-afp.org/entries/Mission_Time_LTL_Language_Partition.html #ITP #IsabelleHOL npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "La felicidad es darse cuenta que nada es demasiado importante." ~ Antonio Gala (1930-2023). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared March 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/04-readings_shared_03-04-25 #AI #AlphaGeometry #CompSci #ITP #LLMs #LeanProver #Logig #Math #Programming #Reasoning #SMT npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso CuDIP: Enhancing theorem proving in LLMs via curriculum learning-based direct preference optimization. ~ Shuming Shi et als. https://arxiv.org/abs/2502.18532 #AI #LLMs #ATP #Logic #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Había un leñador que se agotaba malgastando su tiempo y sus energías en cortar madera con un hacha embotada, porque no tenía tiempo, según él, para detenerse a afilar la hoja." ~ Anthony de Mello (1931-1987). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso How to deepen your understanding of Mizar. ~ Alex Nelson. https://thmprover.wordpress.com/2025/02/22/how-to-deepen-your-understanding-of-mizar/ #ITP #Mizar npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "La civilización avanza ampliando el número de operaciones importantes que podemos realizar sin pensar en ellas." ~ Alfred North Whitehead (1861-1947). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Lambda calculus and Lisp, part 2. https://babbagefiles.xyz/lambda-calculus-and-lisp-02-recursion/ #LambdaCalculus #Emacs #Lisp npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Intro to proofs for the morbidly curious. ~ Evan Chen (2024). https://web.evanchen.cc/handouts/NaturalProof/NaturalProof.pdf #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Formal analysis of electrical circuit network topologies using theorem proving, ~ Kubra Aksoy, Adnan Rashid1, Osman Hasan, Sofiene Tahar. https://ohasan.seecs.nust.edu.pk/Conferences_25/Conferences/SYSCON_2025.pdf #ITP #IsabelleHOL npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Formalisation of combinatorial optimisation in Isabelle/HOL: Network flows. ~ Thomas Ammer. https://youtu.be/8NijQB2oqKg #ITP #IsabelleHOL #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Exercitium: Lista cuadrada. https://jaalonso.github.io/exercitium/posts/2025/02/20-lista_cuadrada/ #Haskell #Python #CommonLisp npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared February 16, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/16-readings_shared_02-16-25 #CategoryTheory #FunctionalProgramming #Haskell #LLMs #LambdaCalculus #Logic #Reasoning npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso 50 years of programming language evolution through the software Heritage looking glass. ~ Adèle Desmazières, Roberto Di Cosmo, Valentin Lorentz. https://hal.science/hal-04924849/document #Programming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper et als. https://arxiv.org/abs/2408.15332 #LLMs #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Competitive programming with large reasoning models. ~ OpenAI. https://arxiv.org/abs/2502.06807 #LLMs #Programming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. https://arxiv.org/abs/2502.00212 #LLMs #ITP #LeanProver #IsabelleHOL npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/turner-bird-eratosthenes-an-eternal-burning-thread/32E2EDF5D5EAEC95F13D313BC97B86F0 #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "La vejez empieza cuando se pierde la curiosidad." ~ José Saramago (1922-2010). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Supercede’s house style for Haskell. ~ Jezen Thomas. https://jezenthomas.com/2025/01/style-guide/ #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Modeling dataframes in Haskell using higher-kinded types. ~ Laurent P. René de Cotret. https://laurentrdc.xyz/posts/HKTGenerics.html #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Bauble: A playground for making 3D art with lisp and math. ~ Ian Henry et als. https://github.com/ianthehenry/bauble #JanetLang #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso A toy example of a verified compiler. ~ Marcus Rossel. https://github.com/marcusrossel/verified-compiler #ITP #LeanProver npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Language models and structured data. ~ Mehwish Alam. https://zenodo.org/records/14673347 #LLMs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso How I program with LLMs. ~ David Crawshaw. https://arstechnica.com/ai/2025/01/how-i-program-with-llms/ #LLMs #Programming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Neuro symbolic reasoning and learning. ~ Paulo Shakarian, Chitta Baral, Gerardo I. Simari, Bowen Xi, Lahari Pokala. https://books.google.nl/books?id=sgfXEAAAQBAJ&newbks=1&newbks_redir=0&lpg=PP1&hl=es&pg=PP1#v=onepage&q&f=false #Logic #AI #MachineLearning npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. https://arxiv.org/abs/2501.09418 #ITP #Coq #Rocq #Logic npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #MULCIA: PhD position in knowledge representation and reasoning, University of Luxembourg. https://tinyurl.com/23a6k25e #PhD #CompSci npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Exercitium: Suma de los números amigos menores que n. https://jaalonso.github.io/exercitium/posts/2025/01/16-suma_de_numeros_amigos_menores_que_n/ #Haskell #Python #Matemáticas npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Vertex algebras in Mathlib: coming soon? ~ Scott Carnahan. https://youtu.be/bmqEmc1nkkU #ITP #LeanProver #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "No hay peor sordo que el que no puede oír; pero hay otro peor, aquél que por una oreja le entra y por otra se le va." ~ Baltasar Gracián (1601-1658). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "En la boca del viejo todo lo bueno fue, y todo lo malo es." ~ Baltasar Gracián (1601-1658). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared January 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/14-readings_shared_01-14-25 #ITP #IsabelleHOL #Coq #Rocq #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared January 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/11-readings_shared_01-11-25 #ITP #LeanProver #Coq #Rocq #Agda #FunctionalProgramming #Haskell #Python #Math #CategoryTheory #ComputerSci #Education #GenAI npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Shallowly embedded functions. ~ Mart Lubbers, Pieter Koopman, Niek Janssen. https://trendsfp.github.io/abstracts/paper-007.pdf #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre Corbineau, Basile Gros, Jean-François Monin. https://hal.science/hal-04859450v1/file/jfla2025-final36.pdf #ITP #Coq #Rocq npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso @nprofile…yy3k Teaching "Foundations of mathematics" with the LEAN theorem prover (Master's Thesis). https://user.math.uzh.ch/cattaneo/bottoni.pdf #ITP #LeanProver #Logic #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Teaching "Foundations of mathematics" with the LEAN theorem prover (Master's Thesis). https://www.math.uzh.ch/typo3conf/ext/qfq/Classes/Api/download.php?s=678105c4a1633 #ITP #LeanProver #Logic #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Un comparador de modelos de Inteligencia Artificial. ~ @Alvy. https://www.microsiervos.com/archivo/ia/comparador-modelos-inteligencia-artificial.html #AI #LLMs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Neuro-Symbolic AI in 2024: A systematic review. ~ Brandon C. Colelough, William Regli. https://arxiv.org/abs/2501.05435 #AI #NeuroSymbolicAI npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. https://bora.uib.no/bora-xmlui/handle/11250/3170892 #ITP #Agda #HoTT npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Typechecking of overloading in programming languages and mechanized mathematics. ~ Arthur Charguéraud, Martin Bodin, Louis Riboulet. https://inria.hal.science/hal-04859446/document #OCaml #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Vérification de bout en bout d’une fonction de bibliothèque mathématique. ~ Paul Geneau de Lamarlière. https://inria.hal.science/hal-04859533/document #ITP #Coq #Rocq #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Los beneficios de otras actividades llegan a aquellos que han llegado al final de un camino difícil, pero en el estudio de la filosofía el placer va a la par del conocimiento creciente; porque el placer no sigue al aprendizaje; más bien, el aprendizaje y el placer avanzan uno al lado del otro." ~ Epicuro (-341, -271). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Formal proof of transcendence of the number e (Part I). ~ Yasushige Watase. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0008 #ITP #Mizar #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. https://arxiv.org/abs/2412.20878 #ITP #IsabelleHOL npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared December 30, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/30-readings_shared_12-30-24 #ITP #Coq #Rocq #FunctionalProgramming #Haskell #CommonLisp #EmacsLisp #Emacs #Logic #Math #CategoryTheory #AI npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Historias de la IA: los autómatas. ~ Manuel de León. https://www.madrimasd.org/blogs/matematicas/2024/12/30/150806 #IA #Autómatas npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Category theory illustrated. ~ Jencel Panic. https://abuseofnotation.github.io/category-theory-illustrated/00_about/ #CategoryTheory npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared December 27, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/27-readings_shared_12-27-24 #ITP #IsabelleHOL #Math #Teaching #AI #LLMs #Emacs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Dibujando figuras con Emacs. ~ Notxor. https://notxor.nueva-actitud.org/2024/12/26/dibujando-figuras-con-emacs.html #Emacs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. https://arxiv.org/abs/2412.16543 #AI #LLMs #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Exercitium: Reconocimiento de potencias de 4. https://jaalonso.github.io/exercitium/posts/2022/02/04-reconocimiento_de_potencias_de_4/ #Haskell #Python npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid (@nprofile…rs4v). https://leanfirststeps.blogspot.com/2024/12/20-contradictory-cases.html #ITP #LeanProver #Lean4 #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared December 24, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/24-readings_shared_12-24-24 #ITP #Agda #Haskell #FunctionalProgramming #Haskell #Python #AI #LLMs #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #Exercitium: El teorema de Navidad de Fermat. https://www.glc.us.es/~jalonso/exercitium/14-dic-23/ #Haskell #Python #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Can AI do maths yet? Thoughts from a mathematician. ~ Kevin Buzzard (@xenaproject.bsky.social). https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/ #AI #ITP #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. https://arxiv.org/abs/2412.16075 #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Isabelle quick start guide. ~ Lawrence Paulson (@nprofile…47al). https://lawrencecpaulson.github.io//2024/12/20/Quickstart.html #ITP #IsabelleHOL #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Una sucesión de pequeñas voluntades consigue un gran resultado." ~ Charles Baudelaire (1821-1867). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Formalize the octonions. ~ Alex Nelson (@pqnelson.bsky.social). https://thmprover.wordpress.com/2024/12/19/formalize-the-octonions/ #ITP #Mizar #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared December 19, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/19-readings_shared_12-19-24 #ITP #IsabelleHOL #Mizar #Logic #Math #Haskell #FunctionalProgramming #LLMs npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid (@nprofile…rs4v). https://leanfirststeps.blogspot.com/2024/12/19-reductio-ad-absurdum.html #ITP #LeanLang #Lean4 #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso 'Lean-style' tactics in Knuckledragger. ~ Philip Zucker (@sandmouth.bsky.social). https://www.philipzucker.com/knuckle_lemma/ #Logic #SMT #Z3 #Python npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Constructive theory of ordinals. ~ Thierry Coquand, Henri Lombardi, Stefan Neuwirth. https://arxiv.org/abs/2201.04352 #Logic #Math #SetTheory npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared December 9, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/09-readings_shared_12-09-24 #ITP #LeanLang #Lean4 #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso "Se comprende mucho mejor un mapa, cuando se le puede hacer por uno mismo. El mejor recurso para comprender, es producir." ~ Immanuel Kant (1724-1804). npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Efficient, portable, census-polymorphic choreographic programming. ~ Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near. https://arxiv.org/abs/2412.02107 #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso (Re)imagining mathematics in a world of reasoning machines. ~ Akshay Venkatesh. https://youtu.be/vYCT7cw0ycw #Math #ITP #AI npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso QuickSub: Efficient iso-recursive subtyping. ~ Litao Zhou, Bruno C.D.S. Oliveira. https://ltzhou.com/static/POPL25extended.pdf #ITP #Coq #Rocq npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Logic and linear algebra: An introduction. ~ Daniel Murfet. https://arxiv.org/abs/1407.2650v3 #Logic #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Proofs of "If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab" in Lean4. https://jaalonso.github.io/calculemus/posts/2024/12/02-tendsto_mul/ #ITP #Lean4 #Math #Calculemus npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Lean: First steps (15 - Zero product). ~ Tariq Rashid (@nprofile…rs4v). https://youtu.be/k2sGtzGGK6k #ITP #Lean4 #Math npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared November 28, 2024. https://jaalonso.github.io/vestigium/posts/2024/11/28-readings_shared_11-28-24 #ITP #IsabelleHOL #Logic #Math #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso #MULCIA: Tenure-track assistant professorship in foundations of computer science with a focus on logic and automated reasoning at Lund University. https://tinyurl.com/27kb4x4u #Job #CompSci npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Axiomatic set theory (Version of 23 November 2024). ~ Tom Leinster. https://www.maths.ed.ac.uk/~tl/ast/ast.pdf #Math #SetTheory npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Scientific computing with confidence using typed dimensions. ~ Laurent P. René de Cotret. https://laurentrdc.xyz/posts/typed-dimensions.html #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso The Haskell Unfolder Episode 36: Concurrency and the FFI. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@nprofile…klk6). https://www.youtube.com/live/IMrBTx7aYjs #Haskell #FunctionalProgramming npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw José A. Alonso Readings shared November 18, 2024. https://jaalonso.github.io/vestigium/posts/2024/11/18-readings_shared_11-18-24 #LLMs #Math #Reasoning #Logic #TypeTheory
