#isabellehol — Public Fediverse posts

Formal verification of an explicit counterexample to the jacobian conjecture. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Jacobian_Counterexample.html #IsabelleHOL #ITP #Math

Formal verification of an explicit counterexample to the jacobian conjecture. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Jacobian_Counterexample.html #IsabelleHOL #ITP #Math

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

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

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

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

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

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

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

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

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

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

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

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

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

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