#isabellehol — Public Fediverse posts

Proving total correctness of top-down solvers with widening and narrowing. ~ Sarah Tilscher, Alexandra Graß, Helmut Seidl, Yannick Stade. https://link.springer.com/article/10.1007/s10817-026-09756-x #IsabelleHOL #ITP

Multitape alphabet roundtrip (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. https://isa-afp.org/entries/Multitape_Alphabet_Roundtrip.html #IsabelleHOL #ITP

Multitape alphabet enlargement (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. https://isa-afp.org/entries/Multitape_Alphabet_Enlargement.html #IsabelleHOL #ITP

Multitape alphabet reduction (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. https://isa-afp.org/entries/Multitape_Alphabet_Reduction.html #IsabelleHOL #ITP

Multitape Turing machine substrate (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. https://isa-afp.org/entries/Multitape_TM_Substrate.html #IsabelleHOL #ITP

Trace based semantics for rely guarantee (in Isabelle/HOL). ~ Marialena Hadjikosti, Andrei Popescu, Jamie Wright. https://isa-afp.org/entries/Trace_Based_Rely_Guarantee.html #IsabelleHOL #ITP

Laurent series expansions on an annulus (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Laurent_Annulus.html #IsabelleHOL #ITP #Math

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

Readings shared: 17-23 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/24-readings_shared_08-24-26 #AI4Math #Agda #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #LogicProgramming #Math #Prolog #RocqProver

Constrained input/output logic in HOL: An algebraic embedding. ~ Ali Farjami, Luca Pasetto. https://ceur-ws.org/Vol-4239/paper-Farjami-14.pdf #IsabelleHOL #ITP

Readings shared August 17, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/17-readings_shared_08-17-26/ #AI4Math #ATP #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #SATsolvers

CAPRI: Contract-aware proof repair for Isabelle. ~ Jim Woodcock, Gabriel Leite, Augusto Sampaio, Ran Wei. https://arxiv.org/abs/2608.13459v1 #IsabelleHOL #ITP #LLMs

First-order methods for smooth convex optimization in Isabelle/HOL. ~ Feier Lyu. https://isa-afp.org/entries/Projected_Gradient_Descent.html #IsabelleHOL #ITP #Math

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

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

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

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

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

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

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