The readings shared in Bluesky on 1 April 2025 are

• A small Prolog on the Z3 AST. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #AI #LLMs #ITP #LeanProver
• The disconnect between AI benchmarks and math research (Evaluating AI systems on their ability to be a mathematical copilot). ~ Ralph Furman. #AI #LLMs #Math
• The cultural divide between mathematics and AI (A reflection on cultural differences observed at the 2025 Joint Mathematics Meeting). ~ Ralph Furman. #AI #LLMs #Math
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Razonamiento automático (2010-11)". #ITP #IsabelleHOL #Logic #Math
• Deducción natural en lógica proposicional con Isabelle/HOL. #Lógica #IsabelleHOL
• Deducción natural en lógica de primer orden con Isabelle/HOL. #Lógica #IsabelleHOL
• Introducción a la demostración asistida por ordenador con Isabelle/HOL (versión de 7 de agosto de 2010). #ITP #IsabelleHOL