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