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

#Calculemus: Demostraciones con Lean 4 del Reto 11 (Si aₙ converge a L, entonces |aₙ| converge a |L|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Napoleon's theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Napo... #IsabelleHOL #ITP #Math

Fast chinese remaindering via product trees (in Isabelle/HOL). ~ Manuel Eberl. isa-afp.org/entries/CRT_... #IsabelleHOL #ITP

Palindromic length in free groups: reflections, noncrossing matchings, and Catalan. ~ Junjie Liao. arxiv.org/abs/2609.170... #LeanProver #ITP

Formalization of Sullivan's no wandering domains theorem in Lean. ~ Ziang Li, Yusheng Luo. arxiv.org/abs/2609.160... #LeanProver #ITP #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 10 (Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Strong normalization for Church-style system F (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Syst... #IsabelleHOL #ITP

Greibach’s hardest context-free language (in Isabelle/HOL). ~ Tobias Nipkow. isa-afp.org/entries/Grei... #IsabelleHOL #ITP

#RetoLean4: Enunciado del reto 19 (Las sucesiones convergentes son de Cauchy). t.me/Retos_Matema... #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 18 (Convergencia del producto de sucesiones convergentes). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 9 (Unicidad del límite). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Structuring mathematics in dependent type theory. ~ Cyril Cohen. inria.hal.science/tel-05737923/ #RocqProver #ITP #Math

Mechanizing Gödel's incompleteness theorems and provability logic. ~ Shogo Saitou, Mashu Noguchi. arxiv.org/abs/2609.13780 #LeanProver #ITP #AI4Math