The readings shared in Bluesky on 1 March 2025 are

• Functional pearl: How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #FunctionalProgramming #Haskell
• A combinatorial identities benchmark for theorem proving via automated theorem generation. ~ Beibei Xiong et als. #LLMs #ITP #LeanProver #Math
• Herald: A natural language annotated Lean 4 dataset. ~ Guoxiong Gao et als. #LLMs #ITP #LeanProver #Math
• LeanProgress: Guiding search for neural theorem proving via proof progress prediction. ~ Suozhi Huang et als. #LLMs #ITP #LeanProver