The readings shared in Bluesky on 14 May 2025 are

• Formal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. #ITP #Rocq #CategoryTheory
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #ITP #Rocq #OCaml
• Theorem prover Arend. ~ Fedor Part, Valery Isaev, and Sergey Sinchuk. #ITP #Arend
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver