The readings shared in Bluesky on 27 April 2025 are

• Bitcoinolog: Reason about Bitcoin addresses with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Working with Common Lisp pathnames. ~ Nicolas Martyanoff. #CommonLisp
• AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. #AI #FormalVerification
• Introducing category theory (Version 26 Apr 2025). ~ Peter Smith. #CategoryTheory
• The levels of Emacs proficiency. ~ Vivek Haldar (2011). #Emacs

The readings shared in Bluesky on 25 April 2025 are

• Lean 4 formalization of the logic textbook "Logic Notes" by Lou van den Dries. ~ Will Bradley. #ITP #LeanProver #Logic #Math
• Neural theorem proving: Generating and structuring proofs for formal verification. ~ Balaji Rao, William Eiers, Carlo Lipizzi. #LLMs #ITP #IsabelleHOL
• Mathematical Logic (Math 570) Lecture Notes. ~ Lou van den Drie. #Logic #Math
• Implementing Unsure Calculator in 100 lines of Haskell. ~ Rodrigo Mesquita. #Haskell #FunctionalProgramming
• Integrating effectful and persistent. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Porting song recommendations to Haskell. ~ Mark Seemann. #Haskell #FunctionalProgramming
• Magical Haskell: A friendly approach to modern functional programming, type theory, and artificial intelligence. ~ Anton Antich. #Haskell #FunctionalProgramming #AI
• #Exercitium: Duplicación de cada elemento. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 24 April 2025 are

• On the averaging problem of ideal families related to Frankl's conjecture with formal proof by Lean 4. ~ Masahiro Hachimori, Kenji Kashiwabara. #ITP #LeanProver #Math
• #Exercitium: Sistema factorádico de numeración. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". #LeanProver #IsabelleHOL #Math

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