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

The readings shared in Bluesky on 1 April 2025 are

• A small Prolog on the Z3 AST. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #AI #LLMs #ITP #LeanProver
• The disconnect between AI benchmarks and math research (Evaluating AI systems on their ability to be a mathematical copilot). ~ Ralph Furman. #AI #LLMs #Math
• The cultural divide between mathematics and AI (A reflection on cultural differences observed at the 2025 Joint Mathematics Meeting). ~ Ralph Furman. #AI #LLMs #Math
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Razonamiento automático (2010-11)". #ITP #IsabelleHOL #Logic #Math
• Deducción natural en lógica proposicional con Isabelle/HOL. #Lógica #IsabelleHOL
• Deducción natural en lógica de primer orden con Isabelle/HOL. #Lógica #IsabelleHOL
• Introducción a la demostración asistida por ordenador con Isabelle/HOL (versión de 7 de agosto de 2010). #ITP #IsabelleHOL

The readings shared in Bluesky on 31 March 2025 are

• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• #Exercitium: Elemento más repetido de manera consecutiva. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "Los primos mayores que 2 son impares". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2010-11)". #Logic #Math #CompSci
• Temas de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de deducción natural proposicional. #Logic #Math
• Ejercicios de deducción natural en lógica de primer orden. #Logic #Math

The readings shared in Bluesky on 30 March 2025 are

• Towards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. #ITP #Coq
• Introducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. #ITP #LeanProver
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "La unión del conjunto de los números naturales pares e impares es el conjunto de los naturales". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2010-11)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2010-11). #Haskell #ProgramaciónFuncional
• Ejercicios de "Informática de 1º de Matemáticas" (2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Exámenes de "Programación funcional con Haskell" Vol. 2 (Curso 2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Introducción al cálculo simbólico con Maxima. #CálculoSimbólico #Maxima #Matemáticas

The readings shared in Bluesky on 29 March 2025 are

• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #ITP #LeanProver
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 28 March 2025 are

• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Verified collaboration: How Lean is transforming mathematics, programming, and AI. ~ Leonardo de Moura. #ITP #LeanProver #Math #Programming #AI
• The philosophical problem of induction, and the problem of Fetzer. ~ Lawrence Paulson. #Philosophy #Math #CompSci
• #Exercitium: Emparejamiento binario. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ t = s ∪ t". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2009-10)". #Lógica #Matemática #Computación
• Temas de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Soluciones de exámenes de Lógica informática (2000-07). #Logic #Math #CompSci
• Curso "Programación declarativa (2009-10)". #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Temas de "Programación funcional con Haskell" (2009-10). #Haskell #FunctionalProgramming
• Introducción a la programación lógica con Prolog. #Prolog #LogicProgramming
• Ejercicios de programación funcional con Haskell (versión del 20 de septiembre de 2007). #Haskell #FunctionalProgramming
• Ejercicios de programación lógica con Prolog (Versión de 20 de septiembre de 2007). #Prolog #LogicProgramming

The readings shared in Bluesky on 27 March 2025 are

• Formalization of optimality conditions for smooth constrained optimization problems. ~ Chenyi Li et als. #ITP #LeanProver
• Formalization of algorithms for optimization with block structures. ~ Chenyi Li, Zichen Wang et als. #ITP #LeanProver
• Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. #ITP #Coq #Rocq #Logic
• Automated reasoning in blockchain: Foundations, applications, and frontiers. ~ Hojer Key. #ITP #Blockchain
• Functional programming in Haskell. ~ Graham Hutton. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 41: Generic monoids. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Decomposing a factorial into large factors. ~ Terence Tao. #Math
• Mathematics of the “I Ching”. ~ Peter Rowlett. #Math #TeXLaTeX
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #LogicProgramming #Prolog #CLP
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (s ∩ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 26 March 2025 are

• Formal proof of Dilworth's theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong, Tianming Liu. #AI #Math
• LogicLearner: A tool for the guided practice of propositional logic proofs. ~ Amogh Inamdar et als. #Logic
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• Curso "Informática (2009-10)". #Haskell #ProgramaciónFuncional #Maxima

The readings shared in Bluesky on 25 March 2025 are

• Teaching "Foundations of Mathematics" with the Lean theorem prover. ~ Mattia Luciano Bottoni, Alberto Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Ten Commandments of the Church of Emacs. #Emacs
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ (s ∪ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 24 March 2025 are

• Formal verification of machine learning models in Lean. ~ Matéo H. Petel. #ITP #LeanProver #MachineLearning
• Why Lisp syntax works. ~ Fernando Borretti. #Lisp #Programming
• MathGPT: Your personal math solver (Get instant homework help from your on-demand AI math solver). #AI #LLMs #Math
• MathGPT: una herramienta para resolver problemas matemáticos y ayudar con los deberes. ~ @Alvy. #IA #LLMs #Matemáticas
• Exercitium (Un reto diario de programación). #Exercitium #Haskell #ProgramaciónFuncional
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Programación lógica (2008-09)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2008-09)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL