The readings shared in Bluesky on 23 March 2025 are

• A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
• Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). #ITP #Coq #SetTheory
• A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). #ITP #Coq #SetTheory
• A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu (2020). #ITP #Coq #SetTheory
• A formalization of properties of continuous functions on closed intervals. Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalizing calculus without limit theory in Coq. ~ Yaoshun Fu, Wensheng Yu (2021). #ITP #Coq #Math
• A formalization of topological spaces in Coq. ~ Sheng Yan, Yaoshun Fu, Dakai Guo, and Wensheng Yu (2022). #ITP #Coq #Math #SetTheory
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). #ITP #Coq #Math #SetTheory
• Implementation of Bourbaki's elements of mathematics in Coq: Part one, theory of sets. ~ José Grimm (2009). #ITP #Coq #SetTheory
• Implementation of Bourbaki’s elements of mathematics in Coq: Part two, ordered sets, cardinals, integers. ~ José Grimm (2018). #ITP #Coq #Math
• Concurrent games in Agda. ~ Amy Yin. #ITP #Agda
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s \ (t ∪ u) ⊆ (s \ t) \ u". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 22 March 2025 are

• Non-obvious Haskell idiom: Guard-sequence. ~ kqr. #Haskell #FunctionalProgramming
• Learn Haskell by example. ~ Phillip Hagenlocher. #Haskell #FunctionalProgramming
• #Exercitium: Segmentos maximales con elementos consecutivos. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 21 March 2025 are

• Case study: Verified Vampire proofs in the LambdaPi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suad. #ATP #Vampire #Dedukti
• A hundred pull requests for Liquid Haskell. ~ Facundo Domínguez. #Liquid #Haskell #FunctionalProgramming #SMT
• Artificial intelligence learns to reason. ~ Melanie Mitchell. #AI #LLMs #Reasoning
• #Exercitium: Lista cuadrada. #Haskell #ProgramaciónFuncional
• Demostraciones de "(a ∖ b) ∖ c ⊆ a ∖ (b ∪ c)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2008-09)". #Lógica #Matemática #Computación
• Curso "Programación declarativa (2008-09)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog

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