The readings shared in Bluesky on 23 April 2025 are

• Bullshit universities: the future of automated education. ~ Robert Sparrow, Gene Flenady. #GenerativeAI #Education
• #Exercitium: Suma de cadenas. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]​] ⊆ f[s] ∪ v". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 22 April 2025 are

• The inverse method is a good fit for Datalog theorem proving. ~ Philip Zucker. #Datalog #Logic
• In between myth and reality: AI for math (a case study in category theory). ~ Răzvan Diaconescu. #LLMs #Math
• #Exercitium: Cuadrado más cercano. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ∩ t = f(s ∩ f⁻¹(t)". #LeanProver #IsabelleHOL #Math

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

The readings shared in Bluesky on 20 April 2025 are

• Readings shared April 19, 2025. #Algorithms #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #MachineLearning #Math #Python #SMT #Z3
• Gridbach: Un proyecto para comprobar de forma distribuida la famosa conjetura de Goldbach. ~ @Alvy #Matemáticas
• Gridbach: The grid-computing system that calculates verification of the mathematical problem "Goldbach conjecture". #Math
• #Exercitium: Órbita prima. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 19 April 2025 are

• Knuckledragger: A low barrier proof assistant. ~ Philip Zucker. #ITP #SMT #Z3 #Python
• Neural theorem proving tutorial. ~ Sean Welleck. #MachineLearning #ITP #LeanProver
• Listing prime numbers periodically. ~ Han-Lin Li, Shu-Cherng Fang, Way Kuo, Nianrui Lin. #Math #Algorithms
• #Exercitium: Ordenada cíclicamente. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 18 April 2025 are

• #Exercitium: Eliminación de las ocurrencias aisladas. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 17 April 2025 are

• Formalization of Fraïssé limits in Lean. ~ Gabin Kolly. #ITP #LeanProver #Math
• A readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. #ITP #Agda
• The Haskell Unfolder Episode 42: Logic programming with typedKanren. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 15 April 2025 are

• Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. #ITP #IsabelleHOL
• First-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. #ITP #IsabelleHOL
• Proof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. #ITP #IsabelleHOL
• The Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. #ITP #IsabelleHOL #Math
• Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. ~ Numina & Kimi Team. #LLMs #LeanProver
• Mathematical reasoning & proofs. ~ Alistair Savage. #Math
• Decomposing factorial of 300K as the product of 300K factors larger than 100K. ~ Gustavo. #Programming #RacketLang #FunctionalProgramming #Math
• Emacs Lisp elements (A big picture view of the Emacs Lisp programming language). ~ Protesilaos Stavrou. #Emacs #Lisp
• The Barium experiment. ~ Tom Szilagyi. #CommonLisp
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 13 April 2025 are

• Completeness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. #ITP #IsabelleHOL #Math #SetTheory
• Efficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. #ITP #Coq
• Mathematical reading list (University of Cambridge). #Math
• LLMs can't stop making up software dependencies and sabotaging everything. ~ Thomas Claburn. #AI #LLMs #Programming
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]". #LeanProver #IsabelleHOL #Math
• Curso "Razonamiento automático (2011-12)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 12 April 2025 are

• Evaluating AI's impact on Haskell open source development. ~ Matthew Pickering, Sam Derbyshire. #LLMs #Haskell #FunctionalProgramming
• #Exercitium: Índices de valores verdaderos. #Haskell #ProgramaciónFuncional