The readings shared in Bluesky on 10 April 2025 are

• Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. #ITP #LeanProver #Math
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity (in Isabelle/HOL). ~ Filip Marić, Jelena Markovic. #ITP #IsabelleHOL
• Leanabell-prover: Posttraining scaling in formal reasoning. ~ Jingyuan Zhang et als. #LLMs #ITP #LeanProver
• Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. #LLMs #ITP #IsabelleHOL
• Reasoning about AI’s reasoning. ~ Höjer Key. #AI #LLMs #ITP #ATP
• Search index in 150 lines of Haskell. ~ kqr. #Haskell #FunctionalProgramming
• Distilling PEP 8 for teaching introductory programming. ~ Diana Kirk, Andrew Luxton-Reilly, Ewan Tempero. #Programming
• Why I program in Lisp. ~ Joe Marshall. #CommonLisp #FunctionalProgramming
• From blind solvers to logical thinkers: Benchmarking LLMs' logical integrity on faulty mathematical problems. ~ A M Muntasir Rahman et als. #LLMs #Math #Reasoning
• #Exercitium: Pim, Pam, Pum y divisibilidad. #Haskell #ProgramaciónFuncional #Matemáticas