The readings shared in Bluesky on 22 May 2025 are

• A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. #ITP #ACL2 #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers. ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver
• Lean-SMT: An SMT tactic for discharging proof goals in Lean. ~ Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett. #ITP #LeanProver
• The roots of Lisp. ~ Paul Graham (2002). #Lisp #Programming
• Las raíces de Lisp. ~ Paul Graham (2002). #Lisp #Programming
• LISP, el "lenguaje de DIOS". ~ LinuxChad. #Lisp #Programming