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 (@AdrianSieber). #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