The readings shared in Mastodon on 3 August 2026 are:

• A Lean 4 library for descriptive complexity. ~ Pierre Senellart. #LeanProver #ITP
• AI safety formalization Atlas. ~ Mario Brčić et als. #LeanProver #ITP #AI
• Formalizing flag algebras in Lean. ~ Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang. #LeanProver #ITP #Math
• Formally certifying number field invariants. ~ Alain Chavarri Villarello, Sander R. Dahmen. #LeanProver #ITP #Math
• Learned interventions in Lean 4 grind. ~ Evan Wang, Simon Chess, Sophie Szeto, Theodore Meek. #LeanProver #ITP
• Metaprogramming in Lean 4. ~ Asei Inoue et als. #LeanProver #ITP
• An LLM-based recommendation system for PVS. ~ Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Mauricio Ayala-Rincón. #PVS #ITP #LLMs
• Show me the money: an exercise in proof-driven software understanding. ~ Joseph Tafese, Karthik Nukala, Hassen Saïdi, Natarajan Shankar, Arie Gurfinkel, Giuliano Losa. #PVS #ITP #Autoformalization
• Growing HOLMS: A verified automated prover for Grzegorczyk logic in HOL Light. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi. #HOL_Light #ITP
• Why is it all in the kernel? ~ Lawrence Paulson. #ITP #LeanProver #IsabelleHOL #RocqProver
• Automating the derivation of unification algorithms (A case study in deductive program synthesis). ~ Richard Waldinger. #DeductiveProgramSynthesis
• Pgeon: Generating tableau-based provers from declarative specifications of logical calculi. ~ Romain Sidhoum, Simon Robillard, David Delahaye. #ATP #Logic #Ocaml
• From lecture notes to Lean: Formalizing a textbook on probability theory. ~ Shuo Deng, Kenneth W. Shum. #AI4Math #LeanProver #ITP
• Machine-checked arithmetic bit complexity of the Kannan-Bachem Smith normal form in Lean 4. ~ Junye Ji. #AI4Math #LeanProver #ITP
• Mathematics without mathematicians. ~ Fernando Borretti. #AI4Math
• Open math problems claimed to be solved with AI. ~ Robert Joseph. #AI4Math
• Pramaana solves IMO 2026 in Lean 4 in under 7 hours (Pramaana’s Panini and Hardy systems formalized and proved all six IMO 2026 problems in Lean 4 in under seven hours and for less than $150). ~ Arnav Mehta. #AI4Math #LeanProver #ITP
• Ten advances in mathematics and theoretical computer science. #AI4Math
• The Maxwell conjecture is false. ~ Philip Arathoon, Gavin Ball, Matthew D. Kvalheim. #AI4Math
• VibeMathed: A website tracking mathematical problems solved by AI models - proved or disproved with a model in the loop. #AI4Math
• El correcto uso de los parámetros en un modelo de Inteligencia Artificial. ~ Diego Germán González. #AI
• 2026 Haskell workshop videos now online. #Haskell #FunctionalProgramming
• Existentials on a leash. ~ Colin de Roos. #Haskell #FunctionalProgramming
• New falsify release. ~ Edsko de Vries. #Haskell #FunctionalProgramming
• Quick tips for fast iteration in Haskell. ~ Tom Ellis, Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• Real World Haskell Revived. #Haskell #FunctionalProgramming
• Vibe coding reconsidered. ~ Joe Marshall. #CommonLisp #VibeCoding #AI4Coding
• #RetoLean4: Enunciado del reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 11 (Si la sucesión aₙ converge a L, entonces |aₙ| converge a |L|). #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 11. #LeanProver #ITP #Math