The readings shared in Bluesky on 29 May 2025 are

• Geometric reasoning in Lean: from algebraic structures to presheaves. ~ Kenji Maillard, Yiming Xu. #ITP #LeanProver #Math
• Construire des preuves mathématiques. ~ Thierry Coquand, William Rowe-Pirra. #ITP #Coq
• Formalizing colimits in Cat. ~ Mario Carneiro, Emily Riehl. #ITP #LeanProver
• A collection of formalized statements of conjectures in Lean, using Mathlib. #ITP #LeanProver #Math
• A formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa. #ITP #IsabelleHOL
• Kimina: Interactive mathematical proof assistant. #AI #ITP #LeanProver #Math
• Context-free grammars and languages (in Isabelle/HOL). ~ Tobias Nipkow et als. #ITP #IsabelleHOL
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. #ITP #Agda
• Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. #ITP #Agda
• Implementing Löb’s theorem in Emacs Lisp. ~ John Wiegley. #Emacs #Lisp #Logic #Math