The readings shared in Bluesky on 27 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn. #ITP #LeanProver #Math
• Simprocs for the working mathematician. ~ Yaël Dillies Paul Lezeau. #ITP #LeanProver
• Proof assistants and type theory. ~ Judah Towery. #ITP #LeanProver #Math
• A foundationally verified intermediate verification language. ~ Joshua M. Cohen. #ITP #CoqProver #Wyh3
• The way of code (The timeless art of Vibe Coding). ~ Rick Rubin. #Programming #Tao