José A. Alonso

Readings shared October 7, 2025 The readings shared in Bluesky on 7 October 2025 are: A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaz

Readings shared October 7, 2025. jaalonso.github.io/vestigium/po... #AI_coding #Advent_of_Code #CommonLisp #FunctionalProgramming #Gemini #Haskell #ITP #IsabelleHOL #LLM #Math

#Exercitium: Números con todos sus dígitos primos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

The Mondrian introduction to functional optics The Mondrian introduction to functional optics

The Mondrian introduction to functional optics. ~ Marco Perone. marcosh.github.io/post/2025/10... #Haskell #FunctionalProgramming

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs...

A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. arxiv.org/abs/2501.10127 #ITP #IsabelleHOL

Using an LLM on the Advent of Code. ~ Joe Marshall. funcall.blogspot.com/2025/09/usin... #Advent_of_Code #AI_coding #CommonLisp #Gemini #LLM

"Una pila de piedras deja de ser una pila de piedras en el momento en que un solo hombre la contempla, concibiendo por dentro la imagen de una catedral." ~ Antoine de Saint-Exupéry (1900-1944).

Readings shared October 6, 2025 The readings shared in Bluesky on 6 October 2025 are: An introduction to formal real analysis (Lecture 8: Advanced limit theorems and induction). ~ Alex Kontorovich. #ITP #LeanProver #Math Formal ver

Readings shared October 6, 2025. jaalonso.github.io/vestigium/po... #AI #CoqProver #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Math #PVS #RustLang

YouTube video by Alex Kontorovich Lecture 8, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 10/03/2025

An introduction to formal real analysis (Lecture 8: Advanced limit theorems and induction). ~ Alex Kontorovich. youtu.be/TMM2QnX5BG8 #ITP #LeanProver #Math

Correctness, artificial intelligence, and the epistemic value of mathematical proof. ~ James Owen Weatherall, Jesse Wolfson. philsci-archive.pitt.edu/24324/1/Epis... #Math #AI #ITP

Dynamic programming primer. ~ James Bowen. mmhaskell.com/blog/2025/10... #Haskell #FunctionalProgramming #RustLang

#Exercitium: Matriz permutación. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. www.cs.princeton.edu/~appel/paper... #ITP #CoqProver #Math

Aristotle: IMO-level Automated Theorem Proving We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Ar...

Aristotle: IMO-level automated theorem proving. ~ Tudor Achim et als. arxiv.org/abs/2510.013... #AI #Math #LLMs #ITP #LeanProver

Waitfree linearization of an arbitrary data object. ~ Wim Hendrik Hesselink. dl.acm.org/doi/pdf/10.1... #ITP #PVS

"Hay que disfrutar de todo, pero sin apegarse a nada. Cuando te desapegues, verás cómo disfrutas mucho más de todo, pues serás mucho más libre para recrearte en cada cosa sin quedar fijado a ninguna." ~ Anthony de Mello (1931-1987).

Mathematics This work stresses the illogical manner in which mathematics has developed, the question of applied mathematics as against 'pure' mathematics, and the challenges to the consistency of mathematics' log...

Mathematics: The loss of certainty. ~ Morris Kline

books.google.es/books?id=RNw...

"Sólo hay una verdad absoluta: que la verdad es relativa." ~ André Maurois (1885-1967).

Readings shared October 4, 2025 The readings shared in Bluesky on 4 October 2025 are: Where is mathematics going? ~ Kevin Buzzard. #Math #ITP #LLM Functional data structures and algorithms: A proof assistant approach. ~ Tobias Nipk

Readings shared October 4, 2025. jaalonso.github.io/vestigium/po... #ACL2 #AI #Algorithms #FunctionalProgramming #ITP #IsabelleHOL #LLMs #Math

YouTube video by Simons Foundation Kevin Buzzard - Where is Mathematics Going? (September 24, 2025)

Where is mathematics going? ~ Kevin Buzzard. youtu.be/K5w7VS2sxD0 #Math #ITP #LLM

IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowle...

IMProofBench: Benchmarking AI on research-level mathematical proof generation. ~ Johannes Schmitt et als. arxiv.org/abs/2509.260... #AI #Math #LLMs

A formal Y86 simulator with CHERI features. ~ Carl Kwan , Yutong Xin, William D. Young. repositum.tuwien.at/bitstream/20... #ITP #ACL2

Functional data structures and algorithms: A proof assistant approach. ~ Tobias Nipkow (Ed.) alioh.com/docs/functio... #ITP #IsabelleHOL #FunctionalProgramming #Algorithms

"El mundo hay que fabricárselo uno mismo, hay que crear peldaños que te suban, que te saquen del pozo. Hay que inventar la vida porque acaba siendo verdad." ~ Ana María Matute (1925-2014).

Readings shared October 03, 2025 The readings shared in Bluesky on 03 October 2025 are: Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. #ITP #LeanProver #Mathlib

Readings shared October 3, 2025. jaalonso.github.io/vestigium/po... #AI #ATP #AlphaProof #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib

Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics: A Mathlib Initiative Interview — Renaissance Philanthropy – A brighter future for all through science, technology, and innovatio... Renaissance Philanthropy is launching the Mathlib Initiative to professionalize and scale the world's largest library of computer-verified mathematics. The Mathlib community has created an open-s...

Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. www.renaissancephilanthropy.org/news-and-ins... #ITP #LeanProver #Mathlib #Math

The Mathlib Initiative The Mathlib Initiative supports the development of mathematical libraries in the Lean theorem prover.

The Mathlib initiative (Building the digital foundation of mathematics). mathlib-initiative.org #ITP #LeanProver #Mathlib #Math

YouTube video by Mechanization of mathematics Stephanie Dick: After Math: historical perspectives on automated intelligence

Mathematics in the age of automated proofs: After Math (historical perspectives on automated intelligence). ~ Stephanie Dick. youtu.be/p-Quz60JMKg #AI #Math #ATP

YouTube video by Mechanization of mathematics Thomas Hubert: AlphaProof: From the lab into your hands

Mathematics in the age of automated proofs: AlphaProof (From the lab into your hands). ~ Thomas Hubert. youtu.be/uhwfTOUIeiw #AI #Math #ITP #LeanProver #AlphaProof

YouTube video by Mechanization of mathematics Akshay Venkatesh: What do we tell our students about AI?

Mathematics in the age of automated proofs: What do we tell our students about AI? ~ Akshay Venkatesh. youtu.be/STTvEmBM3rg #Math #AI

#Exercitium: Inserción en árboles binarios de búsqueda. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas