José A. Alonso

Lean metaprogramming etudes: execution is elaboration. ~ Philip Zucker. https://www.philipzucker.com/elab_lean/ #LeanProver #ITP #FunctionalProgramming

#Calculemus: Demostraciones con Lean 4 del Reto 6 (teorema del emparedado). https://jaalonso.github.io/calculemus/posts/2026/06/14-teorema_del_emparedado/ #LeanProver #Math

A beginning for mathematics. ~ Daniel Litt. https://proofsandprompts.com/2026/09/14/a-beginning-for-mathematics/ #AI4Math

Happy, those able to know the causes of things (An essay on LLMs and the Navier-Stokes equation). ~ Nestor Guillen. https://birdsnfrogs.github.io/2026/09/12/Felix_qui_potuit_rerum_cognoscere_causas.html #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 8 (Sucesiones con infinitos términos grandes no convergen a límites pequeños). https://jaalonso.github.io/calculemus/posts/2026/06/28-no_converge_a_limite_pequeno_si_infinitos_terminos_grandes/ #Math

#Calculemus: Demostraciones con Lean 4 del Reto 7 (La composición de funciones inyectivas es inyectiva). https://jaalonso.github.io/calculemus/posts/2026/06/21-composicion_de_funciones_inyectivas/ #LeanProver #Math

Mechanizing Gödel's incompleteness theorems and provability logic. ~ Shogo Saitou, Mashu Noguchi. https://arxiv.org/abs/2609.13780 #LeanProver #ITP #AI4Math

A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs. ~ Shenghao Yang, Yanyan Dong. https://arxiv.org/abs/2609.10579v1 #LeanProver #ITP #AI4Math

Henstock-Kurzweil gauge integral in the non--gaussian regime: a machine-verified construction. ~ Yuri N. Berdinsky. https://arxiv.org/abs/2609.10793v1 #LeanProver #ITP

Stable singularity of the Euler equations on ℝ³. ~ Adarsh Ganeshram, Valentin Duruisseaux, Anima Anandkumar. https://arxiv.org/abs/2609.10867v1 #AI4Math #LeanProver #ITP

«La causa fundamental del problema es que, en el mundo moderno, los estúpidos están ciegamente seguros de sí mismos, mientras que los inteligentes están llenos de dudas.» ~ Bertrand Russell (1872-1970).

The Kolmogorov–Arnold representation theorem (in Lean 4). ~ George A. Constantinides. https://geoconuk.github.io/lean-misc-math/docs/MiscMath/Analysis/KolmogorovArnold.html #LeanProver #ITP #Math

A four-valued graph model for conflict resolution: core framework and a machine-checked formalization in Lean 4. ~ Yukiko Kato. https://arxiv.org/abs/2609.11174 #LeanProver#ITP #Math

«El espíritu libre no tiene convicciones; solo tiene perspectivas. Toda convicción es una prisión de la que el pensamiento debe liberarse constantemente.» ~ Friedrich Nietzsche (1844-1900).

Metaprogramming in Lean 4. ~ Asei Inoue et als. https://leanprover-community.github.io/lean4-metaprogramming-book/ #LeanProver #ITP

Vibe coding reconsidered. ~ Joe Marshall. https://funcall.blogspot.com/2026/07/vibe-coding-reconsidered.html #CommonLisp #VibeCoding #AI4Coding

The fall of the theorem economy (How AI could destroy mathematics and barely touch it). ~ David Bessis. https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy #AI4Math #LeanProver #ITP

Quick tips for fast iteration in Haskell. ~ Tom Ellis, Laurent P. René de Cotret. https://blog.haskell.org/quick-tips-for-fast-iteration-in-haskell/ #Haskell #FunctionalProgramming

#RetoLean4: Enunciado del reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). https://t.me/Retos_Matematicos/109557/142082 #LeanProver #ITP #Math

#Retolean4: Vídeo tutorial sobre cómo resolver el reto 11. https://youtu.be/bktHsoZDWAQ #LeanProver #ITP #Math

Real World Haskell Revived. https://codeberg.org/jaror/real-world-haskell #Haskell #FunctionalProgramming

Learned interventions in Lean 4 grind. ~ Evan Wang, Simon Chess, Sophie Szeto, Theodore Meek. https://arxiv.org/abs/2607.22972v1 #LeanProver #ITP

#RetoLean4: Soluciones del reto 11 (Si la sucesión aₙ converge a L, entonces |aₙ| converge a |L|). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_11.lean #LeanProver #ITP #Math

2026 Haskell workshop videos now online. https://haskell.foundation/news/2026-07-18/hiw-hew-2026-videos.html #Haskell #FunctionalProgramming

Open math problems claimed to be solved with AI. ~ Robert Joseph. https://aimath.robertj1.com/ #AI4Math

Existentials on a leash. ~ Colin de Roos. https://cdfa.github.io/existentials-on-a-leash/ #Haskell #FunctionalProgramming

New falsify release. ~ Edsko de Vries. https://www.well-typed.com/blog/2026/07/falsify-4/ #Haskell #FunctionalProgramming

Formalizing flag algebras in Lean. ~ Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang. https://arxiv.org/abs/2607.23500v1 #LeanProver #ITP #Math

Pgeon: Generating tableau-based provers from declarative specifications of logical calculi. ~ Romain Sidhoum, Simon Robillard, David Delahaye. https://www.researchgate.net/publication/410760278_Pgeon_Generating_Tableau-Based_Provers_from_Declarative_Specifications_of_Logical_Calculi #ATP #Logic #Ocaml

Show me the money: an exercise in proof-driven software understanding. ~ Joseph Tafese, Karthik Nukala, Hassen Saïdi, Natarajan Shankar, Arie Gurfinkel, Giuliano Losa. https://www.researchgate.net/publication/410760112_Show_Me_The_Money_An_Exercise_in_Proof-Driven_Software_Understanding #PVS #ITP #Autoformalization

A Lean 4 library for descriptive complexity. ~ Pierre Senellart. https://github.com/PierreSenellart/descriptive-complexity #LeanProver #ITP

VibeMathed: A website tracking mathematical problems solved by AI models - proved or disproved with a model in the loop. https://vibemathed.com/ #AI4Math

"¡Qué poco se necesita para la felicidad! El sonido de una gaita. — Sin música, la vida sería un error. El alemán se imagina a Dios cantando canciones." ~ Friedrich Nietzsche (1844-1900).

Formalizing Wu-Ritt method in Lean 4. ~ Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, Lihong Zhi. https://arxiv.org/abs/2604.14912 #LeanProver #ITP #AI4Math

A quadratic form generalization of rational dinv. ~ Yifeng Huang. https://arxiv.org/abs/2604.13238 #LeanProver #ITP #AI4Math

Beyond QED: AI, theorem proving, and the quest for beautiful proofs. ~ Natarajan Shankar. https://youtu.be/5O2c1u7j-iM #AI4Math #ITP

Navier-Stokes and Lean. ~ Lance Fortnow. https://blog.computationalcomplexity.org/2026/09/navier-stokes-and-lean.html #LeanProver #AI4Math

Readings shared: 7-13 September, 2026. https://jaalonso.github.io/vestigium/posts/2026/09/13-readings_shared_09-13-26 #AI #AI4Math #ITP #IsabelleHOL #LeanProver #LeanProver#ITP #Logic #Math

«Ser uno mismo en un mundo que intenta incesantemente convertirte en otra cosa es la mayor de las proezas.» ~ Ralph Waldo Emerson (1803-1882).

Teaching mathematics using Verbose Lean. ~ Patrick Massot. https://youtu.be/WWaasetygqU #LeanProver #ITP #Math

"La causa fundamental del problema es que, en el mundo moderno, los estúpidos están absolutamente seguros de sí mismos, mientras que los inteligentes están llenos de dudas." ~ Russell

Lean: How AI and proof automation are changing mathematics. ~ Leonardo de Moura. https://youtu.be/_DLtAulZaXw #LeanProver #ITP #AI4Math

AI safety formalization Atlas. ~ Mario Brčić et als. https://github.com/mbrcic/ai-safety-formalization-atlas #LeanProver #ITP #AI

gptel: Emacs y la IA. ~ Notxor. https://notxor.nueva-actitud.org/2026/09/13/gptel-emacs-y-la-ia.html #Emacs #AI

When inventing is not enough. ~ Lisa Valentini. https://proofsandprompts.com/2026/09/15/when-inventing-is-not-enough/ #AI4Math

«El que persigue el aprendizaje acumula día a día;
el que sigue el Tao pierde día a día.
Pierde y pierde, hasta llegar a la no-acción.
Por la no-acción, nada queda sin hacerse.»

Lao-Tse (siglo VI a.C.)

Monadic second-order logic in HOL: deep and shallow with automated faithfulness. ~ Christoph Benzmueller, Daniel Kirchner. https://arxiv.org/abs/2609.07345v2 #IsabelleHOL #ITP #Logic

«La prueba más clara de la sabiduría es una alegría continua.» ~ Michel de Montaigne (1533-1592),