#isabellehol — Public Fediverse posts

Machine-checked dual-write recovery from a committed log. ~ Andreas Andreakis. https://arxiv.org/abs/2608.00501 #IsabelleHOL #ITP

Machine-checked dual-write recovery from a committed log. ~ Andreas Andreakis. https://arxiv.org/abs/2608.00501 #IsabelleHOL #ITP

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

A formal counterexample to the cost-preserving single-source unsplittable flow conjecture (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html #IsabelleHOL #ITP

A formal counterexample to the cost-preserving single-source unsplittable flow conjecture (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html #IsabelleHOL #ITP

A deep embedding of HOL in HOL: soundness, completeness, consistency. ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/HOL_in_HOL_Deep.html #IsabelleHOL #ITP

A deep embedding of HOL in HOL: soundness, completeness, consistency. ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/HOL_in_HOL_Deep.html #IsabelleHOL #ITP

Isabelle: the last 40 years (and the next). ~ Lawrence Paulson. https://youtu.be/nEf-WVtpEek #IsabelleHOL #ITP

Isabelle: the last 40 years (and the next). ~ Lawrence Paulson. https://youtu.be/nEf-WVtpEek #IsabelleHOL #ITP

Completeness of the Q₀ higher-order logic (in Isabelle/HOL). ~ Asta Halkjær From, Jonathan Julian Huerta Munive, Anders Schlichtkrull. https://isa-afp.org/entries/Q0_Completeness.html #IsabelleHOL #ITP #Logic

Completeness of the Q₀ higher-order logic (in Isabelle/HOL). ~ Asta Halkjær From, Jonathan Julian Huerta Munive, Anders Schlichtkrull. https://isa-afp.org/entries/Q0_Completeness.html #IsabelleHOL #ITP #Logic

How we solved PutnamBench (A look at formally proving undergraduate competition mathematics). https://varto.ai/news/putnambench/ #AI4Math #IsabelleHOL

How we solved PutnamBench (A look at formally proving undergraduate competition mathematics). https://varto.ai/news/putnambench/ #AI4Math #IsabelleHOL

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

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

PutnamBench Leaderboard (Benchmarking formal mathematical reasoning on the Putnam Mathematical Competition). https://trishullab.github.io/PutnamBench/leaderboard #AI4Math #LeanProver #IsabelleHOL #Coq

PutnamBench Leaderboard (Benchmarking formal mathematical reasoning on the Putnam Mathematical Competition). https://trishullab.github.io/PutnamBench/leaderboard #AI4Math #LeanProver #IsabelleHOL #Coq

Verifying and generalizing simultaneous critical pairs. ~ René Thiemann. https://iwc2026.github.io/documents/iwc2026_proceedings.pdf#page=13 #IsabelleHOL #ITP #Math

Verifying and generalizing simultaneous critical pairs. ~ René Thiemann. https://iwc2026.github.io/documents/iwc2026_proceedings.pdf#page=13 #IsabelleHOL #ITP #Math

Readings shared: July 27 – August 3, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/03-readings_shared_08-03-26/ #AI #AI4Math #ATP #Autoformalization #CommonLisp #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Ocaml #PVS #RocqProver

Readings shared: July 27 – August 3, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/03-readings_shared_08-03-26/ #AI #AI4Math #ATP #Autoformalization #CommonLisp #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Ocaml #PVS #RocqProver

Why is it all in the kernel? ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2026/07/30/Collatz.html #ITP #LeanProver #IsabelleHOL #RocqProver

Why is it all in the kernel? ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2026/07/30/Collatz.html #ITP #LeanProver #IsabelleHOL #RocqProver

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

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

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

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

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

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

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