The readings shared in Bluesky on 2 April 2025 are

• Basic probability in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Mathlib #Math
• GOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. #ITP #HOL4
• Unfolding trees breadth-first in Haskell. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Faking ADTs and GADTs in languages that shouldn't have them. ~ Justin Lê. #Haskell #FunctionalProgramming
• Proof or bluff? Evaluating LLMs on 2025 USA math olympiad. ~ Ivo Petrov et als. #LLMs #Math
• TAUT2 (Here you will find various types of randomly-generated, self-correcting logic excercises). #Logic
• Logica (Tools for thought). #Logic
• Curso de programación lógica. ~ Ana Pradera. #Lógica #ProgramaciónLógica #Prolog
• Enseñanza del sistema de deducción natural en lógica proposicional aplicando programación lógica. ~ Joaquín Arias, Iván Ramírez. #Lógica #ProgramaciónLógica #Prolog
• Apuntes de lógica: desde Aristóteles hasta Prolog. ~ Joaquín Arias. #Lógica #ProgramaciónLógica #Prolog
• #Exercitium: Mayor producto de las ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso: Demostración asistida por ordenador (2010-11). #ITP #IsabelleHOL #Lógica