Deterministic context-free languages are closed under complementation (Hopcroft and Ullman). ~ Kaan Taskin, Tobias Nipkow. isa-afp.org/entries/DPDA... #IsabelleHOL #ITP

Work bounds for strongly joinable balanced binary search trees (in Isabelle/HOL). ~ Marco Haucke. isa-afp.org/entries/Join... #IsabelleHOL #ITP

A mechanized formalization of MicroKanren in Agda- ~ Eduardo Henke, Rodrigo Ribeiro. cbsoft.sbc.org.br/2026/data/pa... #Agda #ITP

Verified QBF solving in Isabelle/HOL: a trustworthy baseline for mechanised quantified boolean reasoning. ~ Axel Bergström, Tjark Weber. fmcad.org/FMCAD26/vstt... #IsabelleHOL #ITP

A formalisation of a special case of the union-closed conjecture in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. arxiv.org/abs/2609.208... #IsabelleHOL #ITP

#Calculemus: Demostraciones con Lean 4 del Reto 14 (Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Gödel's and Scott's variants of the ontological argument in Lean 4. ~ Christoph Benzmüller. arxiv.org/abs/2609.268... #LeanProver #ITP #AI4Math

Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. arxiv.org/abs/2511.20550 #IsabelleHOL #ITP #Math

Formal verification of tilt estimation using the Rocq prover. ~ Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro, Holger Thies. arxiv.org/abs/2609.25561 #RocqProver #ITP

The Teichmüller-Tukey lemma (in Isabelle/HOL). ~ Vithor Lindermann Kraisch, Luiz Gustavo Cordeiro. isa-afp.org/entries/Teic... #IsabelleHOL #ITP #Math

A formalization at large (Laver function in Lean). ~ Leheng Chen, Bin Dong, Jiedong Jiang, Zhiyuan Zhang. frenzymath.com/blog/laverta... #LeanProver #ITP #Math

Complement activation. Chronic inflammation. Shared mechanisms across cytopenias.

In a free webinar, learn how a pathway-based approach can sharpen your clinical management of #ITP, #wAIHA, and beyond.

📅 Sept 30 · 10 AM EDT
Register at 👇
https://ow.ly/ck1s50ZPIfv

#Hematology

#Calculemus: Demostraciones con Lean 4 del Reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. arxiv.org/abs/2511.20550 #IsabelleHOL #ITP #AI4Math

A formalisation of a special case of the union-closed conjecture in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. arxiv.org/abs/2609.20876 #IsabelleHOL #ITP

Immune Thrombocytopenia or #ITP is a rare disease causing low platelet counts, making it harder for blood to clot. This can lead to easy bruising, bleeding, and fatigue. This Global ITP Awareness Week, we join the call for education, research & support for ITP.

#Global4ITP #ITPawareness
#HemeSky

Readings shared: 14-20 September, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

#Calculemus: Demostraciones con Lean 4 del Reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Lean-certified infinite counterexamples to written on the Wall II Conjecture 194. ~ Cameron Beeley. arxiv.org/abs/2609.191... #LeanProver #ITP #AI4Math

Descriptive complexity in Lean: completeness by first-order reductions. ~ Pierre Senellart, Anton Gnatenko. arxiv.org/abs/2609.182... #LeanProver #ITP #AI4Math