The readings shared in Bluesky on 15 January 2025 are

• Readings shared January 14, 2025. #ITP #IsabelleHOL #Coq #Rocq #Haskell #FunctionalProgramming
• #Exercitium: Sucesión de números amigos. #Haskell #Matemáticas
• Root systems and root data in Mathlib. ~ Oliver Nash. #ITP #LeanProver
• An introduction to linters. ~ Damiano Testa. #ITP #LeanProver
• Efficient forward reasoning for Aesop. ~ Xavier Généreux, Jannis Limperg. #ITP #LeanProver
• The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory. ~ Emily Riehl. #ITP #LeanProver
• Searching for proof improvements with tryAtEachStep. ~ David Renshaw. #ITP #LeanProver
• From Aristotle to the iPhone. ~ Moshe Vardi. #Logic #Math #CompSci