The Steiner deltoid as the tangent envelope of Wallace-Simson Lines in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Stei...

#IsabelleHOL #ITP #Math

Steiner's line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Stei...

#IsabelleHOL #ITP #Math

Mathematical proof assistants for teaching logic: the LogiKEy methodology. ~ Christoph Benzmüller, David Fuenmayor, Luca Pasetto. arxiv.org/abs/2610.08214

#IsabelleHOL #ITP #Logic

A first introduction to Isabelle/ML metaprogramming: automatic estimation of polynomial degrees. ~ Jonas Bayer, Anna Danilkin, Marco David, Annie Yao. arxiv.org/abs/2610.08359 #IsabelleHOL #ITP

Weekly reads: Sep 28 – Oct 4, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver

Proofs without nominals: Gödel's ontological argument, its shallow embedding, and the open questions of the Monatshefte Notes. ~ Christoph Benzmüller. arxiv.org/abs/2609.36279 #IsabelleHOL #LeanProver #ITP

Readings shared: 21-27 September, 2026. jaalonso.github.io/vestigium/po... #AI4Maht #Agda #ITP #IsabelleHOL #LeanProver #LogicProgramming #Math #Prolog #RocqProver

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

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

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

The Teichmüller-Tukey lemma (in Isabelle/HOL). ~ Vithor Lindermann Kraisch, Luiz Gustavo Cordeiro. isa-afp.org/entries/Teic... #IsabelleHOL #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

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

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

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