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

The readings shared in Bluesky on 16 January 2025 are

• Readings shared January 15, 2025. #ITP #LeanProver #Logic #Math #CompSci #FunctionalProgramming #Haskell
• #Exercitium: Sucesión de números amigos. #Haskell #Python #Matemáticas
• #Exercitium: Suma de los números amigos menores que n. #Haskell #Python #Matemáticas
• Game "An introduction to constructive logic". ~ Mark Fischer et als./#/g/trequetrum/lean4game-logic #ITP #LeanProver #Logic
• Vertex algebras in Mathlib: coming soon? ~ Scott Carnahan. #ITP #LeanProver #Math
• Real world autoformalization. ~ Siddhartha Gadgil. #ITP #LeanProver #Math
• Building a formal verification framework for smart contracts. ~ Jakob von Raumer. #ITP #LeanProver
• The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? ~ Jason Rute. #ITP #LeanProver #AI
• Information theory in Lean: the DPI. ~ Lorenzo Luccioli. #ITP #LeanProver
• A nimble introduction to nimbers. ~ Violeta Hernández Palacios. #ITP #LeanProver #Math
• An agda2hs-compatible representation of exact real arithmetic. ~ Viktor Csimma. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating SAT and SMT solvers on large-scale sudoku puzzles. ~ Liam Davis, Tairan Ji. #SAT #SMT
• The Haskell Unfolder Episode 38: tasting and testing CUDA (map, fold, scan). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• U-MATH: A university-level benchmark for evaluating mathematical skills in LLMs. ~ Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, Alex Myasnikov, Vlad Stepanov, Alexei Miasnikov, Sergei Tilga. #LLMs #Math

The readings shared in Bluesky on 15 January 2025 are

• Readings shared January 14, 2025. #ITP #IsabelleHOL #Coq #Rocq #Haskell #FunctionalProgramming
• #Exercitium: Sucesión de números amigos. #Haskell #Matemáticas
• Root systems and root data in Mathlib. ~ Oliver Nash. #ITP #LeanProver
• An introduction to linters. ~ Damiano Testa. #ITP #LeanProver
• Efficient forward reasoning for Aesop. ~ Xavier Généreux, Jannis Limperg. #ITP #LeanProver
• The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory. ~ Emily Riehl. #ITP #LeanProver
• Searching for proof improvements with tryAtEachStep. ~ David Renshaw. #ITP #LeanProver
• From Aristotle to the iPhone. ~ Moshe Vardi. #Logic #Math #CompSci

The readings shared in Bluesky on 14 January 2025 are

• Readings shared January 13, 2025. #ITP #Coq #Rocq #HOL4 #CommonLisp #Programming #Math
• An Isabelle/HOL framework for synthetic completeness proofs. ~ Asta Halkjær From. #ITP #IsabelleHOL
• An Isabelle formalization of co-rewrite pairs for non-reachability in term rewriting. ~ Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL
• Formalizing simultaneous critical pairs for confluence of left-linear rewrite systems. ~ Christina Kirk, Aart Middeldorp. #ITP #IsabelleHOL
• Formalized Burrows-Wheeler transform. ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #ITP #IsabelleHOL
• Formalizing the one-way to hiding theorem. ~ Katharina Heidler, Dominique Unruh. #ITP #IsabelleHOL
• Further tackling Post correspondence problem and proof generation. ~ Akihiro Omori, Yasuhiko Minamide. #ITP #IsabelleHOL
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq #Rocq
• Hell (Haskell shell): Year in review. ~ Chris Done. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 13 January 2025 are

• Readings shared January 12, 2025. #ITP #Coq #Rocq #Math #HoTT #CommonLisp #LogicProgramming #Prolog #LPTP
• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Rocq
• Coinductive proofs for temporal hyperliveness. ~ Arthur Correnson, Bernd Finkbeiner. #ITP #Coq #Rocq
• Reversible computation with stacks and "Reversible management of failures". ~ Matteo Palazzo, Luca Roversi. #ITP #Coq #Rocq
• Preservation of speculative constant-time by compilation. ~ Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte. #ITP #Coq #Rocq
• Proof recommendation system for the HOL4 theorem prover. ~ Nour Dekhil, Adnan Rashid, Sofiene Tahar. #ITP #HOL4
• The way of Lisp or the right thing. ~ Joe Marshall. #CommonLisp #Programming
• A road to Common Lisp. ~ Steve Losh (2018). #CommonLisp
• cl-digraph: an implementation of a mutable directed graph data structure for Common Lisp. ~ Steve Losh. #CommonLisp #Math