The readings shared in Bluesky on 30 May 2025 are

• Certified algorithms for numerical semigroups in Rocq. ~ Massimo Bartoletti, Stefano Bonzio, Marco Ferrara. #ITP #Rocq #Math
• Agent-based logics in dependent type theory. ~ Colm Baston. #ITP #Agda
• RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Nikita Khramov, Andrei Kozyrev, Gleb Solovev, Anton Podkopaev. #ITP #Rocq #GenerativeAI
• VERINA: Benchmarking verifiable code generation. ~ Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song. #AIforCode #ITP #LeanProver