José A. Alonso @jalonso - Bluesky Profile

#Exercitium: Expresiones aritmética normalizadas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

25.11.2025 17:10 — 👍 0 🔁 0 💬 0 📌 0

Just out: Functional Data Structures, edited by Tobias Nipkow

25.11.2025 12:47 — 👍 9 🔁 2 💬 0 📌 2

Software never fails. ~ kqr. entropicthoughts.com/software-nev... #Programming

25.11.2025 11:32 — 👍 0 🔁 0 💬 0 📌 0

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 ...

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

25.11.2025 11:28 — 👍 1 🔁 0 💬 0 📌 0

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...

REAL-Prover: Retrieval augmented lean prover for mathematical reasoning. ~ Ziju Shen et als. arxiv.org/abs/2505.20613 #ITP #LeanProver #LLMs #Math

25.11.2025 11:24 — 👍 0 🔁 0 💬 0 📌 0

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...

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

25.11.2025 11:20 — 👍 0 🔁 0 💬 0 📌 0

"Cada uno toma los límites de su propia visión como los límites del mundo." ~ Arthur Schopenhauer (1788-1860).

25.11.2025 11:09 — 👍 0 🔁 0 💬 0 📌 0

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

Readings shared November 24, 2025. jaalonso.github.io/vestigium/po... #CompSci #CoqProver #ITP #LeanProver #Logic #Math #Physics #SetTheory #TypeTheory

25.11.2025 11:08 — 👍 1 🔁 0 💬 0 📌 0

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.

A new bridge links the strange math of infinity to computer science. ~ Joseph Howlett. www.quantamagazine.org/a-new-bridge... #Math #CompSci

24.11.2025 18:56 — 👍 2 🔁 0 💬 0 📌 0

YouTube video by Icelandic Centre of Excellence in Theoretical CS Automatic Geometry Theorem Proving Using Polynomial Elaboration | Mauricio Barba da Costa

Automatic geometry theorem proving using polynomial elaboration. ~ Mauricio Barba da Costa et als. youtu.be/1FjQzA8S7Z4 #ITP #LeanProver #Math

24.11.2025 18:49 — 👍 0 🔁 0 💬 0 📌 0

YouTube video by Icelandic Centre of Excellence in Theoretical CS Gödel Mirror: A Paraconsistent Calculus Mechanized in Lean 4 | Jhet Chan

Gödel mirror: A paraconsistent calculus mechanized in Lean 4. ~ Jhet Chan. youtu.be/6WXyGRZ2uU0 #ITP #LeanProver #Logic #Math

24.11.2025 18:45 — 👍 2 🔁 0 💬 0 📌 0

ITP 2025 Lean Workshop - YouTube

ITP 2025 Lean workshop. youtube.com/playlist?lis... #ITP #LeanProver

24.11.2025 18:42 — 👍 3 🔁 0 💬 0 📌 0

Imagine AI advisers that suggest hypotheses and then automatically generate physics‑consistent proofs using Lean4. The future of safe, verifiable AI is here—check out how theorem proving meets large‑language models! #Lean4 #FormalVerification #AI

🔗 aidailypost.com/news/lean4-p...

22.11.2025 23:25 — 👍 2 🔁 1 💬 0 📌 0

A Perspective on Interactive Theorem Provers in Physics Into an interactive theorem provers (ITPs), one can write mathematical definitions, theorems and proofs, and the correctness of those results is automatically checked. This perspective goes over the ...

A perspective on interactive theorem provers in Physics. ~ Joseph Tooby-Smith. advanced.onlinelibrary.wiley.com/doi/10.1002/... #ITP #LeanProver #Physics

24.11.2025 18:38 — 👍 0 🔁 0 💬 0 📌 0

## Automated Formalization and Verification of Concurrent Reactive Systems using Lean 4 and Alloy Analyzer Integration **Abstract:** This paper introduces a novel framework for automated formalization and verification of concurrent reactive systems, leveraging the expressive power of Lean 4’s dependent type theory and the Alloy Analyzer's powerful constraint solving capabilities. We present an integrated system that automatically translates Alloy specifications of concurrent systems (e.g., protocols, distributed algorithms) into Lean 4 code, enabling comprehensive formal verification utilizing Lean’s theorem prover and property checker.

## Automated Formalization and Verification of Concurrent Reactive Systems using Lean 4 and Alloy Analyzer Integration

**Abstract:** This paper introduces a novel framework for automated formalization and verification of concurrent reactive systems, leveraging the expressive power of Lean 4’s…

23.11.2025 23:18 — 👍 3 🔁 2 💬 0 📌 0

LLMs hallucinate, but in critical systems, that's unacceptable. Lean4 brings formal verification to AI - mathematically proving correctness instead of hoping for it. This could be the reliability breakthrough we need for finance, medicine, autonomous systems. #AI #FormalVerification #Lean4

24.11.2025 05:01 — 👍 3 🔁 1 💬 0 📌 0

YouTube video by Alex Kontorovich Lecture 21, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 11/21/2025

An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. youtu.be/ofB8uRHGu-c #ITP #LeanProver #Math

24.11.2025 18:24 — 👍 1 🔁 0 💬 0 📌 0

Set theory with types. ~ Lawrence Paulson. lawrencecpaulson.github.io//2025/11/21/... #Logic #Math #CompSci #SetTheory #TypeTheory

24.11.2025 17:51 — 👍 2 🔁 0 💬 0 📌 0

A Coq-based Axiomatization of Tarski's Mereogeometry During the last decade, the domain of Qualitative Spatial Reasoning, has known a renewal of interest for mereogeometry, a theory that has been initiated by Tarski. Mereogeometry relies on mereology, t...

A Coq-based axiomatization of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. arxiv.org/abs/2511.16705 #ITP #CoqProver

24.11.2025 17:44 — 👍 2 🔁 0 💬 0 📌 0

Tableau methodology for propositional logics We set out a general methodology for producing tableau systems for propositional logics via a tableau metatheory that provides general and formal notions for different tableau systems that vary by sem...

Tableau methodology for propositional logics. ~ T. Jarmuzek, R. Gore. arxiv.org/abs/2511.167... #Logic

24.11.2025 17:42 — 👍 0 🔁 0 💬 0 📌 0

A Topological Rewriting of Tarski's Mereogeometry Qualitative spatial models based on Goodman-style mereology and pseudo-topology often pose problems for advanced geometric reasoning, as they lack true Euclidean geometry and fully developed topologic...

A topological rewriting of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. arxiv.org/abs/2511.127... #ITP #CoqProver

24.11.2025 17:36 — 👍 0 🔁 0 💬 0 📌 0

"Casi todas nuestras penas surgen de nuestras relaciones con los demás. No hay camino más equivocado hacia la felicidad que la mundanidad." ~ Arthur Schopenhauer (1788-1860).

24.11.2025 12:24 — 👍 0 🔁 0 💬 0 📌 0

Readings shared November 23, 2025 The readings shared in Bluesky on 23 November 2025 are: DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof Verified certification

Readings shared November 23, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq

24.11.2025 12:23 — 👍 1 🔁 0 💬 0 📌 0

ITP 2025 Lean Workshop - YouTube

ITP 2025 Lean Workshop videos youtube.com/playlist?lis...

#LeanLang #LeanProver

20.11.2025 13:49 — 👍 2 🔁 2 💬 0 📌 0

Formalising the local compactness of the adele ring The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal proof that the adele ring of a number field is locally compact implemented in the Lean 4 theorem prover. Our work includes the formalisations of new types, including the completion of a number field at an infinite place, the infinite adele ring and the finite $S$-adele ring, as well as formal proofs that completions of a number field are locally compact and that their rings of integers at finite places are compact.

Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. afm.episciences.org/16007 #ITP #LeanProver #Math

21.11.2025 11:34 — 👍 2 🔁 0 💬 0 📌 0

A complete formalization of Fermat's Last Theorem for regular primes in Lean We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formalization.

A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van De Velde, Andrew Yang. afm.episciences.org/16046 #ITP #LeanProver #Math

21.11.2025 11:32 — 👍 1 🔁 0 💬 0 📌 0

Formalizing zeta and L-functions in Lean The Riemann zeta function, and more generally the L-functions of Dirichlet characters, are among the central objects of study in number theory. We report on a project to formalize the theory of these objects in Lean's "Mathlib" library, including a proof of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis

Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. afm.episciences.org/15954 #ITP #LeanProver

21.11.2025 11:27 — 👍 0 🔁 0 💬 0 📌 0

Formalisation des catégories dérives dans Lean/mathlib This paper outlines the formalization of derived categories in the mathematical library of the proof assistant Lean 4. The derived category D(C) of any abelian category C is formalized as the localization of the category of unbounded cochain complexes with respect to the class of quasi-isomorphisms, and it is endowed with a triangulated structure.

Formalization of derived categories in Lean/mathlib. ~ Joël Riou. afm.episciences.org/15978 #ITP #LeanProver

21.11.2025 11:25 — 👍 0 🔁 0 💬 0 📌 0

Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. www.insmi.cnrs.fr/fr/cnrsinfo/... #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda

21.11.2025 11:20 — 👍 0 🔁 1 💬 0 📌 0

Reseña de «DeepMind’s latest - An AI for handling mathematical proofs» En el artículo «DeepMind’s latest: An AI for handling mathematical proofs», se presenta a AlphaProof, un sistema de inteligencia artificial capaz de razonar y realizar demostraciones matemáticas compl

Reseña de «DeepMind’s latest: An AI for handling mathematical proofs». jaalonso.github.io/vestigium/po... #AI #Math #ITP #LeanProver #AlphaProof

21.11.2025 11:02 — 👍 0 🔁 0 💬 0 📌 0

José A. Alonso

Latest posts by jalonso.bsky.social on Bluesky

@jalonso is following 20 prominent accounts