The readings shared in Bluesky on 30 April 2025 are

• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq
• Verified hand-written Lean solutions to HumanEval. ~ Markus Himmel. #ITP #LeanProver