The readings shared in Bluesky on 23 August 2025 are

• Formalizing class field theory. ~ Georgia Harbor-Collins, Mohit Hulse. #ITP #LeanProver #Math
• Decidable equality for indexed data types, take 2. ~ Brent Yorgey. #Agda #FunctionalProgramming #ITP