The readings shared in Bluesky on 25 April 2025 are

• Lean 4 formalization of the logic textbook "Logic Notes" by Lou van den Dries. ~ Will Bradley. #ITP #LeanProver #Logic #Math
• Neural theorem proving: Generating and structuring proofs for formal verification. ~ Balaji Rao, William Eiers, Carlo Lipizzi. #LLMs #ITP #IsabelleHOL
• Mathematical Logic (Math 570) Lecture Notes. ~ Lou van den Drie. #Logic #Math
• Implementing Unsure Calculator in 100 lines of Haskell. ~ Rodrigo Mesquita. #Haskell #FunctionalProgramming
• Integrating effectful and persistent. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Porting song recommendations to Haskell. ~ Mark Seemann. #Haskell #FunctionalProgramming
• Magical Haskell: A friendly approach to modern functional programming, type theory, and artificial intelligence. ~ Anton Antich. #Haskell #FunctionalProgramming #AI
• #Exercitium: Duplicación de cada elemento. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". #LeanProver #IsabelleHOL #Math