#isabellehol — Public Fediverse posts

Readings shared July 27, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/27-readings_shared_07-27-26 #AI #AI4Math #Agda #Aristotle #ITP #IsabelleHOL #LeanProver #Logic #Math #Prolog #RocqProver

On the formal verification of polynomial commitments: two KZG constructions and the algebraic group model. ~ Tobias Rothmann. https://eprint.iacr.org/2026/1490.pdf #IsabelleHOL #ITP

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

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

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

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

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

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

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

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

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

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

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

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

Greedy algorithms for cardinality-constrained submodular maximization. ~ Feier Lyu. https://isa-afp.org/entries/Submodular_Greedy.html #IsabelleHOL #ITP

On the formalisation of Haag-Kastler nets in higher-order logic. ~ Richard H. J. Schmoetten. https://era.ed.ac.uk/server/api/core/bitstreams/0abbb6de-2234-4219-91f5-6eb9853f9263/content #IsabelleHOL #ITP

Formalization of lower-bound certificates for optimal classical planning. ~ Dmitriy Traytel. https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html #IsabelleHOL #ITP

Lean2Isabelle: Factorized cross-assistant proof translation. ~ Guanyu Liu, Jingkun Ma, Derek F. Wong. https://openreview.net/pdf?id=t9iBTo1zBG #AI4Math #LeanProver #IsabelleHOL #ITP