The readings shared in Bluesky on 25 August 2025 are

• Visualizing regular expression NFAs in Lean. ~ Krishna Padmasola. #ITP #LeanProver
• A case study on the effectiveness of LLMs in verification with proof assistants. ~ Barış Bayazıt, Yao Li, Xujie Si. #ITP #Rocq #LLMs
• Big-stop semantics: A simple way to get the benefits of small-step semantics in a big-step judgment. ~ David M Kahn, Jan Hoffmann, Runming Li. #ITP #Agda
• Formalizing axiomatic theories of truth. ~ Bram Swaanen. #ITP #LeanProver #Logic
• Introduction to proofs using Waterproof. ~ Alex van Tilburg. #ITP #Rocq #Waterproof
• Sets & heaps in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Primos equidistantes. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional #Matemáticas