The readings shared in Bluesky on 12 July 2025 are

• A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. #ITP #CoqProver
• Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon #ATP #Prover9 #Math
• Proof theory and logic programming: Computation as proof search. ~ Dale Miller. #Logic #ProofTheory #LogicProgramming
• Teaching logic programming: a review. ~ Serhiy O. Semerikov et als. #LogicProgramming #Prolog #ASP #CLP
• Categorical semantics in Haskell. ~ Mohamed Amine Ayari. #Haskell #FunctionalProgramming #CategoryTheory
• Generic second-order matching, higher-order preunification and pattern unification - Implementations in Haskell. ~ Nikolai Kudasov et als. #Haskell #FunctionalProgramming
• CriticLean: Critic-guided reinforcement learning for mathematical formalization. ~ Zhongyuan Peng et als. #LLMs #ITP #LeanProver #Math
• ¿Por qué los usuarios de Emacs lo usan para todo? ~ Andros Fenollosa (2023). #Emacs