The readings shared in Bluesky on 30 January 2025 are

• Readings shared January 29, 2025. #ITP #IsabelleHOL
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Analytic number theory exponent database. ~ Terence Tao et als. #ITP #LeanProver #Math
• Cellular methods in homotopy type theory. ~ Axel Ljungström, Loïc Pujet. #ITP #Agda

The readings shared in Bluesky on 29 January 2025 are

• Readings shared January 28, 2025. #ITP #LeanProver #Logic #Math #Prolog #LogicProgramming #Racket #FunctionalProgramming
• Mission-time linear temporal logic (in Isabelle/HOL). ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan. #ITP #IsabelleHOL
• Mission-time linear temporal logic to regular expressions (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian. #ITP #IsabelleHOL

The readings shared in Bluesky on 28 January 2025 are

• Readings shared January 26, 2025. #ITP #LeanProver #HOL_Light #Math
• The directed Van Kampen Theorem in Lean. ~ Henning Basoldm, Peter Bruin, Dominique Lawson. #ITP #LeanProver #Math
• The simplicity of Prolog. ~ Ties Westendorp. #Prolog #LogicProgramming
• Beautiful Racket (An introduction to language-oriented programming using Racket). ~ Matthew Butterick. #Racket #FunctionalProgramming
• New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili./#/g/jadabouhawili/knightsandknaves-lean4game #ITP #LeanProver
• Lean for scientists and engineers. ~ Tyler Josephson. #ITP #LeanProver
• lean-mine: A collection of problems solved in Lean. #ITP #LeanProver #Math
• Baby Rudin project: An attempt to formalize every problem in Baby Rudin with natural language description. #ITP #LeanProver #Math
• Homo ratiocinator (Reckoning human). ~ Moshe Vardi. #Logic #Math

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