The readings shared in Bluesky on 9 December 2025 are:

• The equational theories project: Advancing collaborative mathematical research at scale. ~ Terence Tao et als. #ITP #LeanProver #Math
• Formalized Hopfield networks and Boltzmann machines. ~ Matteo Cipollina, Michail Karatarakis, Freek Wiedijk. #ITP #LeanProver
• The story of Erdős problem #1026. ~ Terence Tao. #AI #Math #ITP #LeanProver #Aristotle #AlphaEvolve
• Formalisation of security for federated learning with DP and attacker advantage in IIIf for satellite swarms. ~ Florian Kammüller. #ITP #IsabelleHOL
• Candle: A verified implementation of HOL Light. ~ Oskar Abrahamsson et als. #ITP #HOL4 #HOL_Light
• #Exercitium: Permutación de elementos consecutivos. #Haskell #ProgramaciónFuncional