The readings shared in Bluesky on 10 December 2025 are:

• Complex bounded operators in Isabelle/HOL. ~ Dominique Unruh, José Manuel Rodríguez Caballero. #ITP #IsabelleHOL #Math
• Formalization of Auslander-Buchsbaum-Serre criterion in Lean4. ~ Naillin Guan, Yongle Hu. #ITP #LeanProver #Math
• A certifying proof assistant for synthetic mathematics in Lean. ~ Wojciech Nawrocki et als. #ITP #LeanProver
• An introduction to formal real analysis (Lecture 25: Swapping limits and integrals). ~ Alex Kontorovich. #ITP #LeanProver #Math
• #Exercitium: Representaciones de matrices. #Haskell #ProgramaciónFuncional #Matemáticas