The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 3, 2025. #ITP #Lean4 #IsabelleHOL #Coq #Rocq #Math #FunctionalProgramming #OCaml #Haskell #Python #AI #MachineLearning
• #Exercitium: Caminos en un triángulo. #Haskell #Python #Matemáticas
• Demostraciones con Isabelle/HOL del "Praeclarum theorema" de Leibniz. #ITP #IsabelleHOL #Logic
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als.. #ITP #LeanProver #Math
• Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. #ITP #HOL_Light #Logic
• Ascoli-Arzel`a theorem (Metric space version). ~ Keiichi Miyajima, Hiroshi Yamazaki. #ITP #Mizar #Math
• Universality of measure space. ~ Noboru Endou, Yasunari Shidama. #ITP #Mizar #Math
• Formalization of orthogonal complements of normed spaces. ~ Hiroyuki Okazaki. #ITP #Mizar #Math