The readings shared in Bluesky on 30 January 2025 are

• Readings shared January 29, 2025. #ITP #IsabelleHOL
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Analytic number theory exponent database. ~ Terence Tao et als. #ITP #LeanProver #Math
• Cellular methods in homotopy type theory. ~ Axel Ljungström, Loïc Pujet. #ITP #Agda