The readings shared in Bluesky on 6 September 2025 are

• An introduction to Lean 4. ~ E. Cosme Llópez, L. Gong. #ITP #LeanProver #FunctionalProgramming
• The gap between commercial and open-source LLMs for Olympiad-level math is shrinking. #AI #LLMs #Math