The readings shared in Bluesky on 30 March 2025 are

• Towards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. #ITP #Coq
• Introducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. #ITP #LeanProver
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "La unión del conjunto de los números naturales pares e impares es el conjunto de los naturales". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2010-11)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2010-11). #Haskell #ProgramaciónFuncional
• Ejercicios de "Informática de 1º de Matemáticas" (2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Exámenes de "Programación funcional con Haskell" Vol. 2 (Curso 2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Introducción al cálculo simbólico con Maxima. #CálculoSimbólico #Maxima #Matemáticas

The readings shared in Bluesky on 29 March 2025 are

• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #ITP #LeanProver
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 28 March 2025 are

• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Verified collaboration: How Lean is transforming mathematics, programming, and AI. ~ Leonardo de Moura. #ITP #LeanProver #Math #Programming #AI
• The philosophical problem of induction, and the problem of Fetzer. ~ Lawrence Paulson. #Philosophy #Math #CompSci
• #Exercitium: Emparejamiento binario. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ t = s ∪ t". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2009-10)". #Lógica #Matemática #Computación
• Temas de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Soluciones de exámenes de Lógica informática (2000-07). #Logic #Math #CompSci
• Curso "Programación declarativa (2009-10)". #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Temas de "Programación funcional con Haskell" (2009-10). #Haskell #FunctionalProgramming
• Introducción a la programación lógica con Prolog. #Prolog #LogicProgramming
• Ejercicios de programación funcional con Haskell (versión del 20 de septiembre de 2007). #Haskell #FunctionalProgramming
• Ejercicios de programación lógica con Prolog (Versión de 20 de septiembre de 2007). #Prolog #LogicProgramming

The readings shared in Bluesky on 27 March 2025 are

• Formalization of optimality conditions for smooth constrained optimization problems. ~ Chenyi Li et als. #ITP #LeanProver
• Formalization of algorithms for optimization with block structures. ~ Chenyi Li, Zichen Wang et als. #ITP #LeanProver
• Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. #ITP #Coq #Rocq #Logic
• Automated reasoning in blockchain: Foundations, applications, and frontiers. ~ Hojer Key. #ITP #Blockchain
• Functional programming in Haskell. ~ Graham Hutton. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 41: Generic monoids. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Decomposing a factorial into large factors. ~ Terence Tao. #Math
• Mathematics of the “I Ching”. ~ Peter Rowlett. #Math #TeXLaTeX
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #LogicProgramming #Prolog #CLP
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (s ∩ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 26 March 2025 are

• Formal proof of Dilworth's theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong, Tianming Liu. #AI #Math
• LogicLearner: A tool for the guided practice of propositional logic proofs. ~ Amogh Inamdar et als. #Logic
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• Curso "Informática (2009-10)". #Haskell #ProgramaciónFuncional #Maxima

The readings shared in Bluesky on 25 March 2025 are

• Teaching "Foundations of Mathematics" with the Lean theorem prover. ~ Mattia Luciano Bottoni, Alberto Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Ten Commandments of the Church of Emacs. #Emacs
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ (s ∪ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 24 March 2025 are

• Formal verification of machine learning models in Lean. ~ Matéo H. Petel. #ITP #LeanProver #MachineLearning
• Why Lisp syntax works. ~ Fernando Borretti. #Lisp #Programming
• MathGPT: Your personal math solver (Get instant homework help from your on-demand AI math solver). #AI #LLMs #Math
• MathGPT: una herramienta para resolver problemas matemáticos y ayudar con los deberes. ~ @Alvy. #IA #LLMs #Matemáticas
• Exercitium (Un reto diario de programación). #Exercitium #Haskell #ProgramaciónFuncional
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Programación lógica (2008-09)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2008-09)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

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