The readings shared in Bluesky on 16 December 2024 are

• Readings shared December 15, 2024. #Haskell #FunctionalProgramming #CategoryTheory #AI #ITP #LeanProver #Math
• Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• Bottom-up computation using trees of sublists. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
• 'Lean-style' tactics in Knuckledragger. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• An example of goal-directed, calculational proof. ~ Roland Carl Backhouse, Walter Guttmann, Michael Winter. #Logic
• Pascal Costanza's Highly Opinionated Guide to Lisp. ~ Pascal Costanza. #CommonLisp #Programming
• Proposing and solving olympiad geometry with guided tree search. ~ Chi Zhang et als. #AI #Math

The readings shared in Bluesky on 15 December 2024 are

• Readings shared December 13, 2024. #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #Haskell #FunctionalProgramming #CategoryTheory
• The future of Math with o1 reasoning with Terence Tao, Mark Chen, and James Donovan. #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 13 December 2024 are

• Readings shared December 12, 2024. #ITP #LeanLang #Lean4 #Math
• On extending incorrectness logic with backwards reasoning. ~ Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran. #ITP #IsabelleHOL
• Machine checked proofs and programs in algebraic combinatorics. ~ Florent Hivert. #ITP #Coq #Rocq #Math
• Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. #ATP #Prover9 #Mace4 #Logic #Math

The readings shared in Bluesky on 12 December 2024 are

• Readings shared December 11, 2024. #ITP #IsabelleHOL #Logic #Math #SetTheory #Haskell #FunctionalProgramming
• Fermat’s Last Theorem — how it’s going. ~ Kevin Buzzard. #ITP #LeanLang #Lean4 #Math

The readings shared in Bluesky on 11 December 2024 are

• Readings shared December 10, 2024. #Haskell #Python #Math #Logic #SMT #Z3 #Python #LLMs #Prolog #LogicProgramming
• Isomorphic transfer infrastructure for nested types in Isabelle/HOL (Work in progress). ~ Gergely Buday, Andrei Popescu. #ITP #IsabelleHOL
• When is a call stack not a call stack? ~ Chris Smith. #Haskell #FunctionalProgramming
• Gödel's program in set theory. ~ Sandra Müller, Grigor Sargsyan. #Logic #Math #SetTheory
• Constructive theory of ordinals. ~ Thierry Coquand, Henri Lombardi, Stefan Neuwirth. #Logic #Math #SetTheory

The readings shared in Bluesky on 10 December 2024 are

• Readings shared December 9, 2024. #ITP #LeanLang #Lean4 #Haskell #FunctionalProgramming
• #Exercitium: Suma fila del triángulo de los impares. #Haskell #Python #Matemáticas
• Dyckhoff intuitionistic propositional prover. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• Enhancing mathematical reasoning in LLMs with background operators. ~ Jiajun Chen, Yik-Cheung Tam. #LLMs #Prolog #LogicProgramming

The readings shared in Bluesky on 9 December 2024 are

• Readings shared December 8, 2024. #ITP #Agda #Coq #Haskell #FunctionalProgramming
• Information sign: Search and coupling (Metavariables, coupling, and formal proofs). ~ Leni Aniva. #ITP #LeanLang #Lean4
• Debugging your Haskell application with debuggable. ~ Edsko de Vries. #Haskell #FunctionalProgramming
• Myth and truth in Haskell asynchronous exceptions. ~ Kazu Yamamoto. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 8 December 2024 are

• Readings shared December 6, 2024. #Haskell #FunctionalProgramming #AI #LLMs #ITP #Math
• Gradual guarantee via step-indexed logical relations in Agda. ~ Jeremy G. Siek. #ITP #Agda
• Explicit weakening. ~ Philip Wadler. #ITP #Agda
• Formally verified hardening of C programs against hardware fault injection. ~ Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet. #ITP #Coq
• Efficient, portable, census-polymorphic choreographic programming. ~ Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 6 December 2024 are

• Readings shared December 5, 2024. #ITP #LeanLang #Lean4 #Coq #Rocq #IsabelleHOL #Logic #Math #FunctionalProgramming #Haskell #OCaml #AI #LLMs
• You could have invented Fenwick trees. ~ Brent A. Yorgey. #Haskell #FunctionalProgramming
• AI for Math fund. ~ Terence Tao. #AI #ITP #Math
• (Re)imagining mathematics in a world of reasoning machines. ~ Akshay Venkatesh. #Math #ITP #AI
• On program synthesis and Large Language Models (Why it is unlikely new developments in machine intelligence will eventually make programming obsolete). ~ Hans Hüttel. #AI #LLMs #Programming
• Pourquoi existe-t-il de nombreux paradigmes de programmation? ~ Oscar Plaisant, Max Lemoine. #Programming #CompSci

The readings shared in Bluesky on 5 December 2024 are

• Readings shared December 4, 2024. #ITP #LeanLang #Logic #Math
• Lean: First steps (18 - Our Own Definition). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• QuickSub: Efficient iso-recursive subtyping. ~ Litao Zhou, Bruno C.D.S. Oliveira. #ITP #Coq #Rocq
• Tail modulo cons, OCaml, and relational separation logic. ~ Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer. #ITP #Coq #OCaml #FunctionalProgramming
• The tensor product on Hilbert spaces (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL #Math
• The Haskell Unfolder Episode 37: Solving Advent of Code 2024 day 4. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems. ~ Roozbeh Yousefzadeh, Xuenan Cao. #LLMs #ITP #LeanLang #Lean4 #Math
• Amplifying human performance in combinatorial competitive programming. ~ Petar Veličković, Alex Vitvitskyi, Larisa Markeeva, Borja Ibarz, Lars Buesing, Matej Balog, Alexander Novikov. #AI #LLMs #Math
• OnlineProver: First experience with teaching formal proofs. ~ Joachim Kristensen et als. #Logic #Teaching