The readings shared in Bluesky on 23 September 2025 are:

• Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• A formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz et als. #ITP #IsabelleHOL #Math
• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Formalizing splitting in Isabelle/HOL. ~ Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. #ITP #IsabelleHOL
• Formalizing the hidden number problem in Isabelle/HOL. ~ Sage Binder, Eric Ren, and Katherine Kosaian. #ITP #IsabelleHOL #Math
• Abstract, compositional consistency: Isabelle/HOL locales for completeness à la Fitting. ~ Asta Halkjær From, Anders Schlichtkrull. #ITP #IsabelleHOL #Logic
• An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems. ~ Dohan Kim. #ITP #IsabelleHOL
• Animating MRBNFs: Truly modular binding-aware datatypes in Isabelle/HOL. ~ Jan van Brügge, Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL
• Improving the SMT proof reconstruction pipeline in Isabelle/HOL. ~ Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. #ITP #IsabelleHOL
• Nondeterministic asynchronous dataflow in Isabelle/HOL. ~ Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. #ITP #IsabelleHOL
• Verifying an efficient algorithm for computing Bernoulli numbers. ~ Manuel Eberl and Peter Lammich. #ITP #IsabelleHOL #Math
• Verification of the CVM algorithm with a functional probabilistic invariant. ~ Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, and Yong Kiam Tan. #ITP #IsabelleHOL
• A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• Finiteness of symbolic derivatives in Lean. ~ Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner. #ITP #LeanProver #Math
• Formalizing colimits in Cat. ~ Mario Carneiro and Emily Riehl. #ITP #LeanProver #CategoryTheory
• Canonical for automated theorem proving in Lean. ~ Chase Norman and Jeremy Avigad. #ITP #LeanProver
• Algebra is half the battle: Verifying presentations of graded unipotent Chevalley groups. ~ Eric Wang et als. #ITP #LeanProver #Math
• Automatically generalizing proofs and statements. ~ Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers. #ITP #LeanProver
• Verifying datalog reasoning with Lean. ~ Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. #ITP #LeanProver
• LeanLTL: A unifying framework for linear temporal logics in lean. ~ Eric Vin, Kyle A. Miller, and Daniel J. Fremont. #ITP #LeanProver
• Certified implementability of global multiparty protocols. ~ Elaine Li and Thomas Wies. #ITP #Rocq
• Formalizing concentration inequalities in Rocq: Infrastructure and automation. ~ Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. #ITP #Rocq
• Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot and Thomas Portet. #ITP #Rocq
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs. #ITP #Rocq
• Towards automating permutation proofs in Rocq: A reflexive approach with iterative deepening search. ~ Nadeem Abdul Hamid. #ITP #Rocq
• Formalising subject reduction and progress for multiparty session processes. ~ Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida. #ITP #CoqProver
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. #ITP #Agda
• A verified cost model for call-by-push-value. ~ Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. #ITP #HOL4
• GOL in GOL in HOL: Verified circuits in Conway’s game of life. ~ Magnus O. Myreen and Mario Carneiro. #ITP #HOL4
• Mechanising Böhm trees and λη-completeness. ~ Chun Tian and Michael Norrish. #ITP #HOL4
• Barendregt’s theory of the λ-calculus, refreshed and formalized. ~ Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. #ITP #Abella
• A natural language formalization of perfectoid rings in ℕaproche. ~ Peter Koepke. #ITP #Naproche #Math
• Adhesive category theory for graph rewriting in Rocq. ~ Samuel Arsac, Russ Harmer, Damien Pous. #ITP #Rocq
• Writing our own structure: Tries in Haskell & Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang