The readings shared in Bluesky on 11 March 2025 are

• Extrinsic termination proofs for well-founded recursion in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Knuth Bendix solver on Z3 AST. ~ Philip Zucker. #SMT #Z3
• Books on the history of mathematics, some thoughts. ~ Thony Christie. #Math
• LLMs can find mathematical reasoning mistakes by pedagogical chain-of-thought. ~ Zhuoxuan Jiang et als. #LLMs #Math
• Can proof assistants verify multi-agent systems? ~ Julian Alfredo Mendez, Timotheus Kampik. #MAS #FormalVerification #LeanProver #Scala
• DeepSeek vs. ChatGPT vs. Claude: A comparative study for scientific computing and scientific machine learning tasks. ~ Qile Jiang, Zhiwei Gao, George Em Karniadakis. #LLMs #Math
• Why do researchers care about small language models? ~ Stephen Ornes. #LLMs #SMLs
• Navigating between points with registers. ~ Daniel Liden. #Emacs
• #Exercitium: Ordenación por el máximo. #Haskell
• #Calculemus: Reto f(f(f(b))) = f(b). #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2002-03)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2003-04)". #LogicProgramming #Prolog #AI
• Curso "Razonamiento automático (2003-04)". #ATP #Otter #Mace #ITP #Jape #PVS
• Curso "Lógica informática (2004-05)". #Logic #Math
• Curso "Programación declarativa (2004-05)". #LogicProgramming #Prolog