The readings shared in Bluesky on 28 September 2025 are:

• Nondeterministic asynchronous dataflow in Isabelle/HOL. ~ Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel. #ITP #IsabelleHOL
• Formalizing splitting in Isabelle/HOL. ~ Ghilain Bergeron, Florent Krasnopol, Sophie Tourret. #ITP #IsabelleHOL
• L-mosaics and bounded join-semilattices in Isabelle/HOL. ~ Alessandro Linzi. #ITP #IsabelleHOL
• Reaping the first fruits of the Isabelle/RL project. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL
• Formalizing the Dershowitz-Manna ordering theorem in Lean 4. ~ Haitian Wang. #ITP #LeanProver
• An introduction to formal real analysis (Lecture 6: Advanced proof techniques and the squeeze theorem). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet. #ITP #Rocq
• Quantifiers for differentiable logics in Rocq. ~ Jairo Miguel Marulanda-Giraldo et als. #ITP #Rocq
• Theorem provers and the future AI math ecosystem. ~ Stephan Schulz. #AI #Math #LLMs #ATP
• Monads are too powerful: The expressiveness spectrum. ~ Chris Penner. #Haskell #FunctionalProgramming
• #Exercitium: Sucesiones pucelanas. #Haskell #ProgramaciónFuncional #Matemáticas