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

The readings shared in Mastodon on 24 November 2024 are

• Readings shared November 23, 2024. #Math #SetTheory #Bluesky
• Lean: First steps (Appendix B - Libraries). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Papers with computer-checked proofs. ~ Daniel J. Bernstein. #ITP
• Does AI mean the end of teaching programming? ~ Alfred Thompson. #AI #Programming #Education
• Are Large Language Models memorizing bug benchmarks? ~ Daniel Ramos, Claudia Mamede, Kush Jain, Paulo Canelas, Catarina Gamboa, Claire Le Goues. #LLMs #Programming

The readings shared in Mastodon on 23 November 2024 are

• Readings shared November 22, 2024. #Logic #Math #FCA #ConExp #AI
• 'A place of joy': why scientists are joining the rush to Bluesky. ~ Smriti Mallapaty. #Bluesky
• Axiomatic set theory (Version of 23 November 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on 22 November 2024 are

• Readings shared November 21, 2024. #ITP #Lean4 #Coq #Haskell #OCaml #FunctionalProgramming #ITP #Prolog #LogicProgramming #Math
• The elementary theory of free Steiner triple systems. ~ Silvia Barbina, Enrique Casanovas. #Logic #Math
• FCA (Formal Concept Analysis) using the Concept Explorer in 2024. ~ Edith Vargas-GarcÍa, Andreas Wachtel. #FCA #ConExp
• Conferencia Leonardo Torres Quevedo: ¿Puede pensar una máquina? ~ Francisco A. González Redondo y Alfonso Hernando González. #AI