The readings shared in Bluesky on 27 June 2025 are

• Formalizing a proof in Lean by hand. ~ Terence Tao. #ITP #LeanProver #Math
• A formalization of the Ionescu-Tulcea theorem in Mathlib. ~ Etienne Marion. #ITP #LeanProver #Math
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Redefinitions in Mizar. ~ Alex Nelson. #ITP #Mizar #Math
• Position: Formal mathematical reasoning (a new frontier in AI). ~ Kaiyu Yang et als. #AI #LLMs #Math #AI4Math #ITP
• LOGICPO: Efficient translation of NL-based logical problems to FOL using LLMs and preference optimization. ~ Koushik Viswanadha, Deepanway Ghosal, Somak Aditay. #LLMs #Math #Autoformalization