Lightnews — Scholar-powered news

José A. Alonso @jalonso.bsky.social · 4h

"Así como no sentimos la salud de todo nuestro cuerpo sino solo el punto donde nos aprieta el zapato, tampoco pensamos en todos nuestros asuntos que marchan perfectamente bien sino en alguna pequeñez insignificante que nos disgusta." ~ Arthur Schopenhauer (1788-1860).

José A. Alonso @jalonso.bsky.social · 4h

Readings shared October 8, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib

Readings shared October 8, 2025

The readings shared in Bluesky on 8 October 2025 are: Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Mic

jaalonso.github.io

Reposted by José A. Alonso

Patrick Shafto @patrickshafto.bsky.social · 1d

Exciting opportunity for people at the intersection of math, AI, and formal methods!

University of Michigan Math search: advanced assistant, or tenured associate or full professor for our initiative on Foundations of Artificial Intelligence
mathjobs.org/jobs/list/26...

1

Reposted by José A. Alonso

Paysages Mathématiques @paysmaths.bsky.social · 22h

"My whole life, my ambition as a mathematician, or rather my joy and my passion, have always been to discover the obvious things." – Alexandre Grothendieck (1928-2014)
#quote #mathematics #math #maths

Photographic portrait of Alexandre Grothendieck, and a quote : "My whole life, my ambition as a mathematician, or rather my joy and my passion, have always been to discover the obvious things."

4 5

José A. Alonso @jalonso.bsky.social · 22h

#Exercitium: Cadenas de ceros y unos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

José A. Alonso @jalonso.bsky.social · 1d

#MULCIA: Göteborgs universitet | Researcher in type theory for mathematics and computer science. tinyurl.com/2bqmjl6e #PostDoc #CompSci

Researcher in type theory for mathematics and computer science

The department of Computer Science and Engineering is strongly international, with approximately 300 employees from

tinyurl.com

José A. Alonso @jalonso.bsky.social · 1d

Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa. arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib #Math

Growing Mathlib: maintenance of a large scale mathematical library

The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding ma...

arxiv.org

1 3

José A. Alonso @jalonso.bsky.social · 1d

"El reto de la modernidad es vivir sin ilusiones y sin desilusionarse." ~ Antonio Gramsci (1891-1937).

José A. Alonso @jalonso.bsky.social · 1d

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

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

jaalonso.github.io

José A. Alonso @jalonso.bsky.social · 1d

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

José A. Alonso @jalonso.bsky.social · 1d

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

The Mondrian introduction to functional optics

marcosh.github.io

2 4

José A. Alonso @jalonso.bsky.social · 1d

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

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

arxiv.org

1 1

José A. Alonso @jalonso.bsky.social · 1d

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

1

José A. Alonso @jalonso.bsky.social · 2d

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

José A. Alonso @jalonso.bsky.social · 2d

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

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

jaalonso.github.io

José A. Alonso @jalonso.bsky.social · 2d

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

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

YouTube video by Alex Kontorovich

youtu.be

3

José A. Alonso @jalonso.bsky.social · 2d

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

2

José A. Alonso @jalonso.bsky.social · 2d

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

3

José A. Alonso @jalonso.bsky.social · 2d

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

1 1

José A. Alonso @jalonso.bsky.social · 3d

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

José A. Alonso @jalonso.bsky.social · 3d

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

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

arxiv.org

José A. Alonso @jalonso.bsky.social · 3d

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

José A. Alonso @jalonso.bsky.social · 3d

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

José A. Alonso @jalonso.bsky.social · 3d

Mathematics: The loss of certainty. ~ Morris Kline

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

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

books.google.es

1

José A. Alonso @jalonso.bsky.social · 4d

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

1 1