The readings shared in Bluesky on 8 April 2025 are

• DMTL4: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Course Cs2120f24: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Training making math proofs using Lean 4. ~ Krillof. #ITP #LeanProver #Math
• PEIRCE: Unifying material and formal reasoning via LLM-driven neuro-symbolic refinement. ~ Xin Quan, Marco Valentino, Danilo S. Carvalho, Dhairya Dalal, André Freitas. #AI #LLMs #ITP #IsabelleHOL #Prolog #LogicProgramming
• #Exercitium: Reiteración de una función. #Haskell #ProgramaciónFuncional #Matemáticas
• [#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f⁻¹[fs ⊆ s"]]. #LeanProver #IsabelleHOL #Math