The readings shared in Bluesky on 19 March 2025 are

• A trickier lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. #LLMs #Programming #FormalVerification
• Towards AI-assisted academic writing. ~ Daniel J. Liebling et als. #AI #LLMs
• VisuAlgo: Visualising data structures and algorithms through animation. #Programming #CompSci
• VisuAlgo muestra visualmente cómo funcionan los algoritmos, las estructuras de datos y cómo resolver problemas. ~ @Alvy. #Programación #Computación
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 19 March 2025 are

• #Exercitium: Máximos locales. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 18 March 2025 are

• Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. #SMT #Z3
• Teaching logic programming: a review. ~ Serhiy O. Semerikov, Iryna S. Mintii, Natalia V. Moiseienko. #LogicProgramming #Prolog #ASP #CLP #Datalog
• Series vs. streams. ~ Joe Marshall. #CommonLisp
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostrar con Isabelle/HOL que las relaciones reflexivas y circulares son simétricas. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2007-08)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog
• Curso "Programación lógica (2007-08)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2007-08)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 17 March 2025 are

• The calculated typer. ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema del barbero. #IsabelleHOL #Lógica

The readings shared in Bluesky on 16 March 2025 are

• Permutations with no consecutive elements. ~ John D. Cook. #Math #Python #Programming
• #Exercitium: Anagramas. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 15 March 2025 are

• Revisiting an early critique of formal verification. ~ Lawrence Paulson. #ITP #Math #FormalVerification
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• Principles of rule-based programming. ~ Thom Frühwirth. #CHR #Constraint #LogicProgramming
• Mathematics for inference and machine learning. ~ Marc Deisenroth, Stefanos Zafeiriou. #Math #MachineLearning
• Introducción a la Introducción de Emacs. ~ Notxor. #Emacs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema de los infectados. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2006-07)". #LogicProgramming #Prolog #AI #NLP #Constraints #Logic
• Curso "Lógica informática (2007-08)". #Lógica #Matemática #Computación

The readings shared in Bluesky on 14 March 2025 are

• La théorie des types, de Russell aux assistans à la demostration. ~ Thierry Coquand. #TypeTheory #ITP #Logic #Math
• Local look-ahead guidance via verifier-in-the-loop for automated theorem proving. ~ Sara Rajaee, Kumar Pratik, Gabriele Cesa, Arash Behboodi. #LLMs #LeanProver
• Algebra, topology, differential calculus, and optimization theory for computer science and machine learning. ~ Jean Gallier, Jocelyn Quaintance. #Math #CompSci #MachineLearning
• Las matemáticas son, sobre todo, hermosas. ~ Marta Macho-Stadler. #Matemáticas
• #Exercitium: Mastermind. #Haskell #FunctionalProgramming
• #Calculemus: La dama o el tigre. #IsabelleHOL #Lógica
• Curso "Razonamiento automático (2005-06)". #ATP #Otter #Mace #ITP #PVS
• Curso "Lógica informática (2006-07)". #Logic #Math #CompSci

The readings shared in Bluesky on 13 March 2025 are

• Course notes for "Formalising Mathematics 2025". ~ Bhavik Mehta et als. #ITP #LeanProver #Math
• LeanAgent: Lifelong learning for formal theorem proving. ~ Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar. #LLMs #ITP #LeanProver #Math
• The Haskell Unfolder Episode 40: Understanding through a model. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Determinación de los elementos minimales. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema lógico del mal. #ITP #IsabelleHOL #Lógica
• Curso "Lógica informática (2005-06)". #Logic #Math #CompSci
• Curso "Programación declarativa (2005-06)". #LogicProgramming #Prolog

The readings shared in Bluesky on 12 March 2025 are

• A formal proof of the irrationality of ζ(3) in Lean 4. ~ Junqi Liu, Jujian Zhang, Lihong Zhi. #ITP #LeanProver #Math
• #Exercitium: La bandera tricolor. #Haskell
• #Calculemus: Teorema de Nicómaco. #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2004-05)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2004-05)". #LogicProgramming #Prolog #AI #NLP #Constraints #MachineLearning
• Curso "Razonamiento automático (2004-05)". #ATP #Otter #Mace #Jape #Logic #ITP #PVS

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