The readings shared in Bluesky on 17 July 2025 are

• Teaching mathematics with Lean: Interactive theorem provers in the classroom. ~ Paola Iannone, Gihan Marasingha, Athina Thoma. #ITP #LeanProver #Math
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak, Vladimir Kolmogorov. #ITP #LeanProver #Math
• Scott's representation theorem and the univalent Karoubi envelope. ~ Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens. #ITP #Rocq
• #Exercitium: Problemas de programación con Haskell de enero de 2021. #Haskell #FunctionalProgramming