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