Readings shared February 11, 2025
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