The readings shared in Bluesky on 19 September 2025 are:

• Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. #ITP #LeanProver
• The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction. ~ Arnaud Mayeux, Jujian Zhang. #ITP #LeanProver
• The groupoid-syntax of type theory is a set. ~ Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie. #ITP #Agda
• Mechanizing the meta-theory of session types in Rocq: A tutorial. ~ Marco Carbone, Alberto Momigliano. #ITP #Rocq
• Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. #ITP #CoqProver #Idris2
• The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. #ITP #Agda