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

The readings shared in Bluesky on 4 December 2024 are

• Readings shared December 3, 2024. #ITP #LeanLang #IsabelleHOL #Coq #Rocq #Math #LLMs #ChatGPT
• Verified foundations for differential privacy. ~ Markus de Medeiros et als. #ITP #LeanLang
• Logic and linear algebra: An introduction. ~ Daniel Murfet. #Logic #Math

The readings shared in Bluesky on 3 December 2024 are

• Readings shared December 2, 2024. #ITP #LeanLang #Math #Calculemus #CategoryTheory #Math #Racket #FunctionalProgramming
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• All your base are belong to U^s (Sort polymorphism for proof assistants). ~ Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter. #ITP #CoqLang #Rocq
• Mechanised safety verification for a distributed autonomous railway control system. ~ Robert Sachtleben, Anne Haxthausen, Jan Peleska. #ITP #IsabelleHOL
• The mathematician who—incidentally—helped mathematicians to stop worrying and love the computer. ~ Keith Devlin. #Math
• ChatGPT turns two: how the AI chatbot has changed scientists’ lives (How many researchers are using the AI tool? Nature gathers data and talks to members of the academic community). ~ Mariana Lenharo. #LLMs #ChatGPT

The readings shared in Bluesky on 2 December 2024 are

• Readings shared December 1, 2024. #ITP #IsabelleHOL #Math
• Proofs of "If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab" in Lean4. #ITP #Lean4 #Math #Calculemus
• Lean: First steps (15 - Zero product). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (16 - Writing our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Category theory in programming. ~ Noah Ma. #CategoryTheory #Math #Racket #FunctionalProgramming