The readings shared in Bluesky on 1 June 2025 are

• A Lean companion to "Analysis I". ~ Terence Tao. #ITP #LeanProver #Math
• AutoGPS: Automated geometry problem solving via multimodal formalization and deductive reasoning. ~ Bowen Ping et als. #MathAI
• An infinitely large napkin. ~ Evan Chen. #Math