The readings shared in Bluesky on 21 October 2025 are:

• HITrees: Higher-order interaction trees. ~ Amir Mohammad Fadaei Ayyam, Michael Sammler. #ITP #LeanProver
• Certifying optimal MEV strategies with Lean. ~ Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino. #ITP #LeanProver
• Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Muntac: A verified certificate checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. #ITP #IsabelleHOL
• RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Andrei Kozyrev, Nikita Khramov, Gleb Solovev, Anton Podkopaev. #ITP #Rocq #LLMs
• #Exercitium: Listas equidigitales. #Haskell #ProgramaciónFuncional #Matemáticas