The readings shared in Bluesky on 26 January 2025 are

• Readings shared January 25, 2025. #ITP #Agda #Coq #Rocq #IsabelleHOL #Math #FunctionalProgramming #Haskell #JuliaLang
• Certified knowledge compilation with application to formally verified model counting. ~ Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule. #ITP #LeanProver
• Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. #ITP #HOL_Light #Math
• Math Encounters: "You want proof? I'll give you proof! (Mathematical arguments from Euclid to Lean)". ~ Jeremy Avigad. #ITP #LeanProver #Math

The readings shared in Bluesky on 25 January 2025 are

• Readings shared January 24, 2025. #ITP #IsabelleHOL #Haskell #FunctionalProgramming #AI #LLMs #GenerativeAI #NeuroSymbolicAI
• Pinpointing the learning obstacles of an interactive theorem prover. ~ Sára Juhošová, Andy Zaidman, Jesper Cockx. #ITP #Agda
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Combinatorial q-analogues (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Theta functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• The Rogers–Ramanujan identities (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Use monoids for construction. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Calculus for the modern engineer: Putting the joy back in learning advanced mathematics. ~ Jessy Grizzle. #Math #JuliaLang
• Calculus for the modern engineer (Textbook). ~ Jessy Grizzle et als. #Math #JuliaLang #LLMs

The readings shared in Bluesky on 24 January 2025 are

• Readings shared January 23, 2025. #ITP #IsabelleHOL #LeanProver #Python #Programming #Math #AI #LLMs
• Formally verified neurosymbolic trajectory learning via tensor-based linear temporal logic on finite traces. ~ Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #NeuroSymbolicAI
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Fast Haskell, Redux. ~ Jared Tobin. #Haskell #FunctionalProgramming
• Making my life easier with GADTs. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Making my life harder with GADTs. Matt Parsons. #Haskell #FunctionalProgramming
• Making my life easier with two GADTs. ~ borar. #Haskell #FunctionalProgramming
• Modeling dataframes in Haskell using higher-kinded types. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• Supercede’s house style for Haskell. ~ Jezen Thomas. #Haskell #FunctionalProgramming
• Tracing foreign function invocations. ~ Edsko de Vries, Zubin Duggal, Matthew Pickering. #Haskell #FunctionalProgramming
• What I've learned about writing AI apps so far. ~ Laurie Voss. #AI #LLMs
• AI mistakes are very different than human mistakes. ~ Bruce Schneier, Nathan E. Sanders. #AI #LLMs #GenerativeAI
• Cómo trabajar en el día a día con una IA y no morir en el intento. ~ @Alvy. #AI #LLMs
• DeepSeek: un nuevo modelo de IA especializado en razonamiento lógico, resolución de problemas y con licencia abierta MIT. No tiene nada que envidiar a los de OpenAI. ~ @Alvy. #AI #LLMs #DeepSeek
• DeepSeek: Into the unknown (Free access to DeepSeek-V3). #AI #LLMs #DeepSeek

The readings shared in Bluesky on 23 January 2025 are

• Readings shared January 22, 2025. #ITP #IsabelleHOL #Coq #Rocq #LeanProver #FunctionalProgramming #Haskell #Python #Math #AI
• Formalising an easy proof: Dirichlet's approximation theorem. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Hallucination detection and recovery: Initial experiment. ~ GasStationManager. #LLMs #ITP #LeanProver
• Advanced Python course. ~ Michael Foord. #Python #Programming
• ELIZA, la primera psicoterapeuta programada con IA, rescatada del olvido gracias a la arqueología informática. ~ @Alvy. #IA

The readings shared in Bluesky on 22 January 2025 are

• Readings shared January 21, 2025. #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
• #Exercitium: Iguales al siguiente. #Haskell #Python #Matemáticas
• Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Advent of Code 2024: Haskell solution reflections for all 25 days. ~ Justin Le. #Haskell #FunctionalProgramming
• Scientific computing in Lean. ~ Tomas Skrivan. #ITP #LeanProver #Math
• Alpha-beta pruning explored, extended and verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• Can a computer judge interestingness? ~ Michael Douglas. #AI #Math
• Formalising real algebraic geometry. ~ Artie Khovanov, Michael Nedzelsky, Wenda Li. #ITP #IsabelleHOL #Math
• The Mandelbrot set is connected (and other Lean explorations). ~ Geoffrey Irving. #ITP #LeanProver #Math
• Formalising theory of combinatorial optimisation. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
• Condensed type theory. ~ Johan Commelin. #ITP #LeanProver #Math
• How to prove Fermat's Last Theorem. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Structures in dependent type theory. ~ Jeremy Avigad. #ITP #LeanProver
• Comparative formalisation of Kneser's theorem. ~ Mantas Bakšys, Yaël Dillies. #ITP #IsabelleHOL #LeanProver #Math
• Lawvere theories in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
• How to teach Fourier analysis to a large library of formalised mathematics. ~ Yaël Dillies. #ITP #LeanProver #Math
• Computer algebra and the formalisation of new mathematics. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• New Foundations: the story of a large formalisation project. ~ Sky Wilshaw. #ITP #LeanProver #Math
• The mathematics of Artificial Intelligence. ~ Gabriel Peyré. #AI #Math
• The Ramanujan Library (Automated discovery on the hypergraph of integer relations). ~ Itay Beit-Halachmi, Ido Kaminer. #Math #CompSci
• Wikenigma: An encyclopedia of unknowns. #Math #CompSci

The readings shared in Bluesky on 21 January 2025 are

• Readings shared January 20, 2025. #ITP #LeanProver #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #CommonLisp #JanetLang #AI #LLMs #Programming
• Proofs of the Praeclarum Theorema in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing domino tilings with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Think of a number. ~ Kevin Buzzard. #AI #LLMs #Math
• Negatively associated random variables (in Isabelle/HOL). ~ Emin Karayel. #ITP #IsabelleHOL #Math
• Las series de Kempner, o qué ocurre cuando quito un dígito. ~ Miguel Ángel Morales. #Matemáticas

The readings shared in Bluesky on 20 January 2025 are

• Readings shared January 19, 2025. #ITP #LeanProver #FunctionalProgramming #Haskell #AI #LLMs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #Python #Matemáticas
• Classifying the groups of order pq in Lean. ~ Scott Harper, Peiran Wu. #ITP #LeanProver #Math
• Certifying rings of integers in number fields. ~ Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen. #ITP #LeanProver #Math
• Lean: First steps (22 - Recursion). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• [Lean: First steps (22 - Recursion) Video]. ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Lean Together 2025. #ITP #LeanProver
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abzulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Interpreting Brainfuck in Haskell. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Hasochism: The pleasure and pain of dependently typed Haskell programming. ~ Sam Lindley, Conor McBride. #Haskell #FunctionalProgramming
• An efficient algorithm for permutation iteration using a singly linked list. ~ Thomas Baruchel. #CommonLisp #Algorithms
• Janet: a functional and imperative programming language. #JanetLang #FunctionalProgramming
• Janet for mortals (a real book). ~ Ian Henry. #JanetLang #FunctionalProgramming
• Bauble: A playground for making 3D art with lisp and math. ~ Ian Henry et als. #JanetLang #FunctionalProgramming
• Building Bauble. ~ Ian Henry #JanetLang #FunctionalProgramming
• Awesome Janet: Curated list of libraries and tooling for the Janet programming language. ~ Matthew Carter. #JanetLang #FunctionalProgramming
• How developers interact with AI: A taxonomy of human-AI collaboration in software engineering. ~ Christoph Treude, Marco A. Gerosa. #AI #LLMs #Programming

The readings shared in Bluesky on 19 January 2025 are

• Readings shared January 18, 2025. #Haskell #Python #CommonLisp #ITP #Coq #Rocq #Logic #Math #AI #MachineLearning #LLMs
• A toy example of a verified compiler. ~ Marcus Rossel. #ITP #LeanProver
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgrammingo
• Foundations of Large Language Models. ~ Tong Xiao, Jingbo Zhu. #eBook #AI #LLMs
• Language models and structured data. ~ Mehwish Alam. #LLMs

The readings shared in Bluesky on 18 January 2025 are

• Readings shared January 17, 2025. #Haskell #Python #ITP #Coq #Rocq #LeanProver #Logic #Math #AI #LLMs #Reasoning
• #Exercitium: Mastermind. #Haskell #Python #Matemáticas
• Formal proofs in applied mathematics: A Coq formalization of simplicial Lagrange finite elements. ~ Houda Mouhcine. #ITP #Coq #Rocq #Math
• Neurosymbolic tools for effective coding and debugging. ~ Georgios Sakkas. #AI #MachineLearning #LLMs
• Iteration. ~ Joe Marshall. #CommonLisp
• Lisp tutorial. ~ Daniel Nussenbaum. #CommonLisp
• Release Common Lisp on your first day. ~ Dan's Musings. #CommonLisp
• Listopia: List manipulation library inspired by Haskell package Data.List. ~ Ito Dimercel. #CommonLisp #Haskell
• Lisp programming language (Full course for beginners). ~ Alberto Lerda. #CommonLisp
• Neuro symbolic reasoning and learning. ~ Paulo Shakarian, Chitta Baral, Gerardo I. Simari, Bowen Xi, Lahari Pokala. #Logic #AI #MachineLearning
• How I program with LLMs. ~ David Crawshaw. #LLMs #Programming

The readings shared in Bluesky on 17 January 2025 are

• Readings shared January 16, 2025. #ITP #LeanProver #Agda #Logic #Math #SAT #SMT #FunctionalProgramming #Haskell #Python #Matemáticas #AI #LLMs
• #Exercitium: Determinación de los elementos minimales. #Haskell #Python #Matemáticas
• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq #Logic
• Scaling mathlib: tooling and automation for an ever-growing mathematics library. ~ Michael Rothgang. #ITP #LeanProver
• Progress report on the Carleson Project. ~ Floris van Doorn. #ITP #LeanProver #Math
• Egg: An equality saturation tactic in Lean. ~ Marcus Rossel et als. #ITP #LeanProver
• lean-SMT. ~ Abdalrhman Mohamed. #ITP #LeanProver
• Toward functor quasi-categories in Lean. ~ Jack McKoen. #ITP #LeanProver
• Verified foundations for differential privacy. ~ Jean-Baptiste Tristan. #ITP #LeanProver
• Can AI models reason: Is data all you need? ~ Wayne Joubert. #AI #LLMs #Reasoning