The readings shared in Bluesky on 25 January 2025 are

• Readings shared January 24, 2025. #ITP #IsabelleHOL #Haskell #FunctionalProgramming #AI #LLMs #GenerativeAI #NeuroSymbolicAI
• Pinpointing the learning obstacles of an interactive theorem prover. ~ Sára Juhošová, Andy Zaidman, Jesper Cockx. #ITP #Agda
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Combinatorial q-analogues (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Theta functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• The Rogers–Ramanujan identities (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Use monoids for construction. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Calculus for the modern engineer: Putting the joy back in learning advanced mathematics. ~ Jessy Grizzle. #Math #JuliaLang
• Calculus for the modern engineer (Textbook). ~ Jessy Grizzle et als. #Math #JuliaLang #LLMs