The readings shared in Bluesky on 3 April 2025 are

• Morley's theorem (in Isabelle/HOL). ~ Benjamin Puyobro. #ITP #IsabelleHOL #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #CategoryTheory #Math #Haskell #FunctionalProgramming
• LeanSolver: Solving theorems through large language models and search. ~ Avi Luciano Halevy #LLMs #ITP #LeanProver
• AlphaProof: when reinforcement learning meets formal mathematics. ~ Thomas Hubert. #AlphaProof #AI #Math
• #Exercitium: Biparticiones de una lista. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". #LeanProver #IsabelleHOL #Math #Calculemus