Perron's formula (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Perrons_Formula.html #IsabelleHOL #ITP #Math

Formalization of template formulas in the modal μ-calculus in Isabelle/HOL. ~ Lise Arendsen. https://pure.tue.nl/ws/portalfiles/portal/390531427/Arendsen_L.pdf #IsabelleHOL #ITP #Logic

Readings shared June 22, 2026. https://jaalonso.github.io/vestigium/posts/2026/06/22-readings_shared_06-22-26 #AI4Math #Agda #ChatGPT #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog

The Dottie number (in Isabelle/HOL). ~ Lawrence C. Paulson. https://isa-afp.org/entries/Dottie_Number.html #IsabelleHOL #ITP #Math

A formalization of the exponential blowup in the transformations between CNF and DNF (in Isabelle/HOL). ~ Leon Raffael Schulz, Martin Desharnais-Schäfer, Jan Johannsen. https://isa-afp.org/entries/CNF_DNF_Exp_Blowup.html #IsabelleHOL #ITP

Formalization of weighted sets (in Isabelle/HOL). ~ Mathias Schack Rabing, Dmitriy Traytel. https://isa-afp.org/entries/Weighted_Set.html #IsabelleHOL #ITP

The detour calculus: Rigorous local deformation of integration contours. ~ Manuel Eberl. https://isa-afp.org/entries/Detour_Calculus.html #IsabelleHOL #ITP #Math

LLMemma: An LLM-guided Isabelle proof synthesis system. ~ Daniel Busing, Hyunkyung Lee, Isaac Mangano, Timothy Stanbrough, Tommy Tran. https://www.researchgate.net/profile/Daniel-Busing/publication/406962966_LLMemma_An_LLM-Guided_Isabelle_Proof_Synthesis_System/links/6a2b502d8ab2ac2a709716b1/LLMemma-An-LLM-Guided-Isabelle-Proof-Synthesis-System.pdf #IsabelleHOL #IYP #LLMs

Formalization of countable multisets (in Isabelle/HOL). ~ Mathias Schack Rabing, Dmitriy Traytel. https://isa-afp.org/entries/Countable_Multiset.html #IsabelleHOL #ITP

Vosper's theorem and the Cauchy–Davenport theorem via the polynomial method. ~ Arthur Freitas Ramos , David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Cauchy_Davenport_Vosper.html #IsabelleHOL #ITP #Math