The readings shared in Bluesky on 24 December 2025 are:

• From zero to QED: An informal introduction to formality with Lean 4. ~ Stephen Diehl. #ITP #LeanProver
• A verified implementation of the Misra and Gries edge coloring algorithm. ~ Arohee Bhoja. #ITP #LeanProver
• Formalising differential geometry in Lean. ~ Michael B. Rothgang. #ITP #LeanProver #Math
• Metaprogramming your IDE in Lean 4. ~ Harry Goldstein, Richard Feldman. #ITP #LeanProver
• Gödel's Poetry. ~ Kelly J. Davis. #ITP #LeanProver #AI #LLMs
• #Exercitium: 2015 y los números pitagóricos. #Haskell #ProgramaciónFuncional #Matemáticas