The readings shared in Bluesky on 17 October 2025 are:

• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Yalep: An environment for learning proof in high-school. ~ Frédéric Tran-Minh, Laure Gonnord, Julien Narboux. #ITP #LeanProver #Logic #Math #Teaching
• Yalep (Yet Another Learning Environment for Proof) is a micro language based on Lean for teaching mathematical high-school proofs. ~ Frédéric Tran Minh. #ITP #LeanProver #Logic #Math #Teaching
• Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord, Julien Narboux. #ITP #Logic #Math #Teaching
• Lean4Less: Eliminating definitional equalities from Lean via an extensional-to-intensional translation. ~ Rishikesh Vaishna. #ITP #LeanProver
• Proof strategy extraction from LLMs for enhancing symbolic provers. ~ Jian Fang, Yican Sun, Yingfei Xiong. #ITP #Rocq #LLM
• Z mathematical toolkit in Isabelle/HOL. ~ Simon Foster, Pedro Ribeiro, Frank Zeyda, Jim Woodcock. #ITP #IsabelleHOL
• MASA: LLM-driven multi-agent systems for autoformalization. ~ Lan Zhang, Marco Valentino, André Freitas. #Autoformalization #LLM #ITP #LeanProver #Math
• Great expectations: Unifying statistical theory and programming. ~ Bradley Saul. #ITP #Agda #FunctionalProgramming #Math
• Where is mathematics going? Large language models and Lean proof assistant. ~ John Elliot V. #Math #LLMs #ITP #LeanProver
• Bridging category theory and functional programming for enhanced learning. ~ Fethi Kadhi. #Haskell #FunctionalProgramming #CategoryTheory
• Exploring Arrows for sequencing effects. ~ Chris Penner. #Haskell #FunctionalProgramming
• Non-obvious Haskell idiom: Bind to lambda case. ~ kqr. #Haskell #FunctionalProgramming
• #Exercitium: Actualización de ejercicios del curso 2014-15. #Haskell #ProgramaciónFuncional #Matemáticas