The readings shared in Bluesky on 21 April 2025 are

• A formalisation of Aristotle’s assertoric syllogistic in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Karol Wapniarski. #ITP #IsabelleHOL #Logic
• Non-circular trigonometric proofs of the pythagorean theorem in Lean4: A comparison. ~ Paul Pajo. #ITP #LeanProver #Math
• Enhancing AI trustworthiness through automated reasoning: A novel method for explaining deep learning and LLM reasoning. ~ Julia Connolly, Oliver Stanton, Sarah Veronica, Liam Whitmore. #LLMs #Reasoning #ITP
• SLip: Lisp system in your browser. ~ Mihai Bazon. #CommonLisp
• #Exercitium: Divisores de un número con final dado. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]​". #LeanProver #IsabelleHOL #Math