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

The readings shared in Bluesky on 1 December 2024 are

• Readings shared November 30, 2024. #Lean4 #FunctionalProgramming
• The sum-of-squares function and Jacobi's two-square theorem (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math

The readings shared in Bluesky on 30 November 2024 are

• Readings shared November 29, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Calculemus #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry #Haskell #FunctionalProgramming #Programming #FormalVerification #Dafny
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #Lean4 #FunctionalProgramming

The readings shared in Bluesky on 29 November 2024 are

• Readings shared November 28, 2024. #ITP #IsabelleHOL #Logic #Math #Haskell #FunctionalProgramming
• Proof of "If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac" in Lean4. #ITP #Lean4 #Math #Calculemus
• Machine learning and mathematics (The twin catalysts poised to accelerate twenty-first century mathematics: formalisation and machine learning). ~ Harald Carlens. #Math #ITP #Lean4 #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry
• Deep embedding of intuitionistic linear logic. ~ Filip Smola, Jacques D. Fleuriot. #ITP #IsabelleHOL #Logic #Math
• Brillo: Painless 2D vector graphics, animations, and simulations powered by GLFW (Fork of gloss). ~ Adrian Sieber. #Haskell #FunctionalProgramming
• Effectiveness of Large Language Models to generate formally verified C code. ~ Merlijn Sevenhuijsen. #LLMs #Programming #FormalVerification
• dafny-annotator: AI-assisted verification of Dafny programs. ~ Gabriel Poesia, Chloe Loughridge, Nada Amin. #LLMs #Dafny #FormalVerification

The readings shared in Bluesky on 28 November 2024 are

• Readings shared November 27, 2024. #Haskell #FunctionalProgramming #AI #MachineLearning #Math
• Semantics for linear-time temporal logic with finite observations. ~ Rayhana Amjad, Rob van Glabbeek, Liam O'Connor. #ITP #IsabelleHOL #Logic #Math
• Competitive Programming in Haskell: stacks, queues, and monoidal sliding windows. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 27 November 2024 are

• Readings shared November 26, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Prolog #LogicProgramming #Z3 #SMT #AI #Education
• Haskell: A great procedural language. ~ kqr. #Haskell #FunctionalProgramming
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #Haskell #FunctionalProgramming
• Linear algebra done right. ~ Sheldon Axler. #eBook #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper, Anibal M. Medina-Mardones, Bartłomiej Lewandowski, Angus Gruen, Piotr Kucharski, Sergei Gukov. #AI #MachineLearning #Math

The readings shared in Mastodon on 26 November 2024 are

• Readings shared November 25, 2024. #ITP #Lean4 #Rocq #FunctionalProgramming #CommonLisp
• Impossibility of the dissection of a cube (in Isabelle/HOL). ~ Thomas Holme Surlykke. #ITP #IsabelleHOL #Math
• Two theorems on hermitian matrices (in Isabelle/HOL). ~ Sage Binder, Zilin Jiang. #ITP #IsabelleHOL #Math
• Ground lambda Prolog. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl. ~ Stefan Neuwirth, Henri Lombardi, Thierry Coquand. #Logic #Math
• Grupos y capturas reemplazando texto con expresiones regulares. ~ Fernando Briano. #Emacs
• Lean: First steps (18 - Our own definition). ~ Tariq Rashid. #ITP #Lean4 #Math
• IA Generativa: Estrategias de uso para docentes desde infantil a bachillerato. ~ Pablo Haya. #AI #Education

The readings shared in Mastodon on 25 November 2024 are

• Readings shared November 24, 2024. #ITP #Lean4 #Math #AI #LLMs #Programming #Education
• Cryptography experiments in Lean 4: SHA-3 implementation. ~ Gérald Doussot. #ITP #Lean4 #FunctionalProgramming
• Scaling up mechanized proof automation for small-step semantics. ~ Sandrine Blazy, Alain Delaët, Denis Merigoux. #ITP #Rocq
• Counting connected components of a graph. ~ Atabey Kaygun. #FunctionalProgramming #CommonLisp