The readings shared in Bluesky on 3 September 2025 are

• Thinking programs (Logical modeling and reasoning about languages, data, computations, and executions). ~ Wolfgang Schreiner. #ITP #IsabelleHOL #Logic #CompSci
• A blueprint for the formalization of Carleson's theorem on convergence of Fourier series. ~ Lars Becker et als. #ITP #LeanProver #Math
• Lean for JavaScript developers. ~ Dan Abramov. #ITP #LeanProver
• Contradiction, contraposition and Lean. ~ Oussama. #ITP #LeanProver
• The meta-principle: A type-theoretic theorem and its interpretation. ~ Jonathan Washburn. #ITP #LeanProver
• Introduction to formal methods using interactive proof assistant Rocq. ~ Evgeny Makarov. #ITP #Rocq
• #Exercitium: Entero positivo de la cadena. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 2 September 2025 are

• Aspects of category theory in proof assistants. ~ Luc Chabassier. #ITP #CoqProver #CategoryTheory
• No-free-lunch theorem for machine learning. ~ Michikazu Hirata. #ITP #IsabelleHOL
• #Exercitium: Actualizaciones de ejercicios. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 1 September 2025 are

• Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. #ITP #LeanProver #Mathlib
• Starting out with graph algorithms: Basic DFS. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• Alpha-beta pruning is just minimax in a lattice of clamping functions. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• #Exercitium: Buscaminas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Mayor sucesión del problema 3n+1. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Filtro booleano. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 31 August 2025 are

• #Exercitium: Descomposiciones como sumas de n sumandos. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Selección hasta el primero que falla inclusive. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 30 August 2025 are

• Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. #ITP #IsabelleHOL
• Demostración incorrecta de P ≠ NP publicada en la revista "Frontiers of Computer Science". ~ Francisco R. Villatoro. #Math
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Número de inversiones. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Eliminación de las ocurrencias aisladas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ordenada cíclicamente. #Haskell #ProgramaciónFuncional
• #Exercitium: Órbita prima. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Divisores de un número con final dado. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 August 2025 are

• Tic-tac-toe meets Lean 4. ~ Adolfo Ochagavía. #ITP #LeanProver
• Continuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda
• Erdös problems. ~ Thomas Bloom. #Math
• #Exercitium: Números triangulares con n cifras distintas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Enumeración de árboles binarios. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Elementos de una matriz con algún vecino menor. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Reiteración de una función. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Pim, Pam, Pum y divisibilidad. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Código de las alergias. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Índices de valores verdaderos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 28 August 2025 are

• Haskell Course: Lesson 21: Reader, Writer, and State Monads. ~ Robertino Martinez. #Haskell #FunctionalProgramming
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Elemento más repetido de manera consecutiva. #Haskell #ProgramaciónFuncional
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Mayor producto de las ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Biparticiones de una lista. #Haskell #ProgramaciónFuncional
• #Exercitium: Trenzado de listas. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 27 August 2025 are

• Basic category theory. ~ Tom Leinster. #eBook #CategoryTheory
• #Exercitium: Segmentos maximales con elementos consecutivos. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 26 August 2025 are

• Experimental results for Vampire on the equational theories project. ~ Mikoláš Janota. #ATP #Vampire
• Lean meets theoretical computer science: Scalable synthesis of theorem proving challenges in formal-informal pairs. ~ Terry Jingchen Zhang et als. #ITP #LeanProver #LLMs
• Why cannot large language models ever make true correct reasoning? ~ Jingde Cheng. #LLMs #Reasoning
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Máximos locales. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Lista cuadrada. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 August 2025 are

• Visualizing regular expression NFAs in Lean. ~ Krishna Padmasola. #ITP #LeanProver
• A case study on the effectiveness of LLMs in verification with proof assistants. ~ Barış Bayazıt, Yao Li, Xujie Si. #ITP #Rocq #LLMs
• Big-stop semantics: A simple way to get the benefits of small-step semantics in a big-step judgment. ~ David M Kahn, Jan Hoffmann, Runming Li. #ITP #Agda
• Formalizing axiomatic theories of truth. ~ Bram Swaanen. #ITP #LeanProver #Logic
• Introduction to proofs using Waterproof. ~ Alex van Tilburg. #ITP #Rocq #Waterproof
• Sets & heaps in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Primos equidistantes. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional #Matemáticas