The readings shared in Bluesky on 4 June 2025 are

• Mathematics in Lean (Release v4.19.0). ~ Jeremy Avigad, Patrick Massot. #ITP #LeanProver #Math
• Functional programming in Lean. ~ David Thrane Christiansen. #ITP #LeanProver #FunctionalProgramming
• The concept of definition: in mathematics, and in computational logic. ~ Lawrence Paulson. #Logic #Math #ITP