Visual Lean: An accessible interface for Lean 4 proofwriting. ~ Autumn Mapes. aitp-conference.org/2026/abstrac... #LeanProver #ITP

The logic of Bunched implications is undecidable, mechanized in Rocq. ~ Dominique Larchey-Wendling. members.loria.fr/DLarchey/fil... #Rocq #ITP

Formalization of Langlands’s first main lemma for local epsilon factors. ~ Fukuhiro Ueda. hal.science/hal-05746185... #LeanProver #ITP #AI4Math

#Vestigium: Formalización del libro "Calculus" de Spivak en Lean 4. jaalonso.github.io/vestigium/po... #LeanProver #ITP #AI4Math

Lean 4 formalization of Michael Spivak's "Calculus" (covering both the 3rd and 4th editions). ~ Jon-Erik G. Storm. github.com/stormj-UH/sp... #LeanProver #ITP #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 15 (Existe un k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. arxiv.org/abs/2509.19632 #LeanProver #ITP #AI4Math

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