The readings shared in Bluesky on 25 July 2025 are

• A formalization of elementary linear algebra: Part I. ~ David Russinoff. #ITP #ACL2 #Math
• A formalization of elementary linear algebra: Part II. ~ David Russinoff. #ITP #ACL2 #Math
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• RV32I in ACL2. ~ Carl Kwan. #ITP #ACL2
• Extended abstract: Partial-encapsulate and its support for floating-point operations in ACL2. ~ Matt Kaufmann, J Strother Moore. #ITP #ACL2
• Lean FRO and Mathlib receive $10M from XTX Markets founder Alex Gerko to further advance the use of AI for mathematical research. #AI4Math #ITP #LeanProver #Math
• A Liquid Haskell kick-start. ~ Xavier Góngora. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de diciembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell de noviembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas