The readings shared in Bluesky on 2 March 2025 are

• Waterproof: Transforming a proof assistant into an educational tool. ~ Aalt Jelle Wemmenhove. #ITP #Coq #Math #Education
• Computer assisted mathematical proofs: using the computer to verify computers. ~ Herman Geuvers. #ITP #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean. ~ Pietro Monticone. #ITP #LeanProver #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean (Codes). ~ Pietro Monticone. #ITP #LeanProver #Math
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Applying purity to the imperative world. ~ Jeremy Bowers. #Haskell #FunctionalProgramming
• ¿Podemos creer la prueba de la conjetura? ~ Marta Macho Stadler. #Math #CompSci