The readings shared in Bluesky on 31 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco et als. #ITP #LeanProver #Math
• Lean4Lean: Mechanizing the metatheory of Lean. ~ Mario Carneiro. #ITP #LeanProver
• HoTTLean: Formalizing the meta-theory of HoTT in Lean. ~ Joseph Hua et als. #ITP #LeanProver #HoTT
• Towards modular composition of inductive types using Lean meta-programming. ~ Ramy Shahin. #ITP #LeanProver
• Löb’s theorem and provability predicates in Rocq. ~ Janis Bailitis1, Dominik Kirst, Yannick Forster. #ITP #Rocq #Logic #Math
• A Coq formalization of Lagois connections for secure information flow. ~ Casper Stahl et als. #ITP #Coq #Rocq
• Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. #ITP #Coq #Rocq #Agda
• Efficient program extraction in elementary number theory using the proof assistant Minlog. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math