José A. Alonso

"La vida oscila como un péndulo entre el sufrimiento y el aburrimiento." ~ Arthur Schopenhauer (1788-1860).

Readings shared March 1, 2026 The readings shared in Bluesky on 1 March 2026 are: Lean for science formalization. ~ Przemyslaw Chojecki. #LeanProver #ITP Vibe-coding a debugger for a DSL. ~ Joachim Breitner. #LeanProver Bidirecti

Readings shared March 01, 2026. jaalonso.github.io/vestigium/po... #ITP #LeanProver #RocqProver

Vibe-coding a debugger for a DSL. ~ Joachim Breitner. www.joachim-breitner.de/blog/819-Vib... #LeanProver

Lean for science formalization. ~ Przemyslaw Chojecki. www.ulam.ai/research/lea... #LeanProver #ITP

Bidirectional interpolation for the lambda-calculus – Revisiting and formalising Craig-Čubrić interpolation. ~ Meven Lennon-Bertrand, Alexis Saurin. hal.science/hal-05526634... #RocqProver #ITP

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof wri...

Machine-generated, machine-checked proofs for a verified compiler (Experience report). ~ Zoe Paraskevopoulou. arxiv.org/abs/2602.20082 #RocqProver #ITP

"Todos los seres florecen, pero cada uno retorna a su raíz. Retornar a la raíz es hallar el reposo. Hallar el reposo es cumplir el destino." ~ Lao-Tse (siglo VI a.C.).

Reseña de «AI that can prove it’s right: Verification as the missing l En el vídeo «AI that can prove it’s right: Verification as the missing layer in AI», Carina Hong explica cómo Axiom Math está desarrollando una inteligencia artificial matemática capaz de autoverifica

Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». jaalonso.github.io/vestigium/po... #AI4Math #LeanProver

"La felicidad es el derecho a la pereza y el deber de la alegría." ~ José Luis Sampedro (1917-2013).

"Nadie es más esclavo que aquel que se cree libre sin serlo, o aquel que busca en las riquezas el remedio para su pobreza de espíritu. El oro y la plata no nos hacen mejores; solo nos hacen más visibles." ~ Lucio Anneo Séneca (c. 4 a.C. – 65 d.C.)

"La esperanza es el sueño del hombre despierto." ~ Aristóteles (384-322 a.C.).

Readings shared February 24, 2026 The readings shared in Bluesky on 24 February 2026 are: Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math Integral curves and flows on Ban

Readings shared February 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedi...

DSLean: A framework for type-correct interoperability between Lean 4 and external DSLs. ~ Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck. arxiv.org/abs/2602.18657 #LeanProver #ITP

Large Language Model Reasoning Failures Large Language Models (LLMs) have exhibited remarkable reasoning capabilities, achieving impressive results across a wide range of tasks. Despite these advances, significant reasoning failures persist...

Large language model reasoning failures. ~ Peiyang Song, Pengrui Han, Noah Goodman. www.arxiv.org/abs/2602.06176 #LLMs #Reasoning

M2F: Automated Formalization of Mathematical Literature at Scale Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as ...

M2F: Automated formalization of mathematical literature at scale. ~ Zichen Wang et als. arxiv.org/abs/2602.170... #AI4Math #ITP #LeanProver

Math in the Age of AI | Communications of the ACM You will be notified whenever a record that you have chosen has been cited.

Math in the age of AI. ~ Allyn Jackson. dl.acm.org/doi/full/10.... #AI4Math

Haskell meets Evariste Since its birth as a new scientific body of knowledge in the late 1950s, computer programming has become a fundamental skill needed in many other disciplines. However, programming is not easy, it is p...

Haskell meets Evariste. ~ Paulo R. Pereira, Jose N. Oliveira. arxiv.org/abs/2602.168... #Haskell #FunctionalProgramming

When Agda met Vampire Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in ...

When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. arxiv.org/abs/2602.188... #Agda #ITP #Vampire #ATP

Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain m...

Formalized run-time analysis of active learning - coalgebraically in Agda. ~ Thorsten Wißmann. arxiv.org/abs/2602.16427 #Agda #ITP

Classifying 2-groups in Homotopy Type Theory. ~ Perry Hart, Owen Milner. phart3.github.io/2-groups-pre... #Agda #ITP

Verifying the Hashgraph Consensus Algorithm The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus wi...

Verifying the hashgraph consensus algorithm. ~ Karl Crary. arxiv.org/abs/2102.011... #CoqProver #ITP

A formal correctness proof of Edmonds’ blossom shrinking algorithm. ~ Mohammad Abdulaziz, Kurt Mehlhorn. link.springer.com/content/pdf/... #IsabelleHOL #ITP

Lean Formalization of Generalization Error Bound by Rademacher Complexity We formalize the generalization error bound using Rademacher complexity in the Lean 4 theorem prover. Generalization error quantifies the gap between a learning machine's performance on given training...

Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. arxiv.org/abs/2503.196... #LeanProver #ITP

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several n...

Nazrin: Atomic tactics for graph neural networks for theorem proving in Lean 4. ~ Leni Aniva, Iori Oikawa, David Dill, Clark Barrett. arxiv.org/abs/2602.187... #LeanProver #ITP

Formalization of Two Fixed-Point Algorithms in Hilbert Spaces Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\uı--Mann iteration and Halpern iteration are two w...

Formalization of two fixed-point algorithms in Hilbert spaces. ~ Yifan Bai, Yantao Li, Jian Yu, Jingwei Liang. arxiv.org/abs/2602.170... #LeanProver #ITP

Integral Curves and Flows on Banach Manifolds in Lean We present a formalisation of the existence and uniqueness theorems of integral curves of vector fields on Banach manifolds in the Lean theorem prover. First, we formalize properties of differential e...

Integral curves and flows on Banach manifolds in Lean. ~ Weichen Winston Yin, Yury Kudryashov. arxiv.org/abs/2602.132... #LeanProver #ITP #Math

Formalizing Gröbner Basis Theory in Lean We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the core foundations of ...

Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. arxiv.org/abs/2602.127... #LeanProver #ITP #Math

"Un hombre solo puede ser él mismo mientras esté solo; si no ama la soledad, no ama la libertad, pues solo cuando se está solo se es libre." ~ Arthur Schopenhauer (1788-1860).

"Vivir es sentirse perdido… El que no acepta que está perdido, se pierde inexorablemente." ~ José Ortega y Gasset (1883-1955).

"Aquellos que no pueden recordar el pasado están condenados a repetirlo." ~ George Santayana (1863-1952).