#isabellehol — Public Fediverse posts

New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP

New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP

Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP

Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP

Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math

Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math

Polynomial commitment schemes (in Isabelle/HOL). ~ Tobias Rothmann. https://isa-afp.org/entries/Polynomial_Commitment_Schemes.html #IsabelleHOL #ITP

Polynomial commitment schemes (in Isabelle/HOL). ~ Tobias Rothmann. https://isa-afp.org/entries/Polynomial_Commitment_Schemes.html #IsabelleHOL #ITP

Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic

Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic

Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic

Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic

Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic

The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Chevalley_Warning.html #IsabelleHOL #ITP #Math

The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Chevalley_Warning.html #IsabelleHOL #ITP #Math

First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. https://bford.info/pub/lang/paradox/paradox.pdf #IsabelleHOL #ITP #Math

Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. https://bford.info/pub/lang/paradox/paradox.pdf #IsabelleHOL #ITP #Math

Readings shared July 13, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/13-readings_shared_07-13-26 #AI4Math #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

Readings shared July 13, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/13-readings_shared_07-13-26 #AI4Math #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Arithmetic_Geometric_Mean.html #IsabelleHOL #ITP #Math

Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Arithmetic_Geometric_Mean.html #IsabelleHOL #ITP #Math

Bessel functions of the first kind (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Bessel.html #IsabelleHOL #ITP #Math

Bessel functions of the first kind (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Bessel.html #IsabelleHOL #ITP #Math

The exponential and logarithmic integral (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Exp_Log_Integral.html #IsabelleHOL #ITP #Math

The exponential and logarithmic integral (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Exp_Log_Integral.html #IsabelleHOL #ITP #Math

Generalised hypergeometric series (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Generalized_Hypergeometric_Series.html #IsabelleHOL #ITP #Math

Generalised hypergeometric series (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Generalized_Hypergeometric_Series.html #IsabelleHOL #ITP #Math

Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. https://isa-afp.org/entries/Rademacher_Series.html #IsabelleHOL #ITP #Math

Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. https://isa-afp.org/entries/Rademacher_Series.html #IsabelleHOL #ITP #Math

The incomplete gamma function (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Incomplete_Gamma.html #IsabelleHOL #ITP #Math

The incomplete gamma function (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Incomplete_Gamma.html #IsabelleHOL #ITP #Math

Correctness and complexity of BMSSP in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/BMSSP_Correctness.html #IsabelleHOL #ITP

Correctness and complexity of BMSSP in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/BMSSP_Correctness.html #IsabelleHOL #ITP

Freiman's 3k - 4 theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Freiman_3k_4.html #IsabelleHOL #ITP #Math

Freiman's 3k - 4 theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Freiman_3k_4.html #IsabelleHOL #ITP #Math

Height bounds for height-balanced trees (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Height_Balanced_Tree_Bounds.html #IsabelleHOL #ITP

Height bounds for height-balanced trees (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Height_Balanced_Tree_Bounds.html #IsabelleHOL #ITP

Axiomatic theory of hereditarily finite sets and its fragments (in Isabelle/HOL). ~ Štěpán Holub, Zuzana Haniková. https://isa-afp.org/entries/ZF_finite.html #IsabelleHOL #ITP #Math

Axiomatic theory of hereditarily finite sets and its fragments (in Isabelle/HOL). ~ Štěpán Holub, Zuzana Haniková. https://isa-afp.org/entries/ZF_finite.html #IsabelleHOL #ITP #Math

Certified infinite descent criteria (in Isabelle/HOL). ~ Jamie Wright, Liron Cohen, Reuben Rowe, Andrei Popescu. https://isa-afp.org/entries/Infinite_Descent_Criteria.html #IsabelleHOL #ITP

Certified infinite descent criteria (in Isabelle/HOL). ~ Jamie Wright, Liron Cohen, Reuben Rowe, Andrei Popescu. https://isa-afp.org/entries/Infinite_Descent_Criteria.html #IsabelleHOL #ITP

Readings shared July 22, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/06-readings_shared_07-06-26 #AI4Math #Agda #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #PVS

Readings shared July 22, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/06-readings_shared_07-06-26 #AI4Math #Agda #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #PVS

Formalization of 3-independence of simple tabulation hashing (in Isabelle/HOL). ~ Wei De Leong, Yong Kiam Tan, Seng Joe Watt. https://isa-afp.org/entries/Tabulation_Hashing.html #IsabelleHOL #ITP

Formalization of 3-independence of simple tabulation hashing (in Isabelle/HOL). ~ Wei De Leong, Yong Kiam Tan, Seng Joe Watt. https://isa-afp.org/entries/Tabulation_Hashing.html #IsabelleHOL #ITP