Readings shared October 17, 2025
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