José A. AlonsoA formal embedding for assessing the complexity of model consistency. ~ Romain Pascual et als. https://assets-eu.researchsquare.com/files/rs-8978072/v1_covered_99de7da6-f305-417a-b332-cbc078feeab3.pdf #IsabelleHOL #ITP
Sorted rewriting, conditional rewriting, and logically constrained rewriting (in Isabelle/HOL). ~ Akihisa Yamada. https://www.isa-afp.org/entries/Sorted_Rewriting.html #IsabelleHOL #ITP
Lebesgue-Stieltjes integral (in Isabelle/HOL). ~ Yosuke Ito. https://www.isa-afp.org/entries/Lebesgue_Stieltjes_Integral.html #IsabelleHOL #ITP #Math
Readings shared March 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/20-readings_shared_02-19-26 #ATP #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Physics #Prover9
Achim D. BruckerWant to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!
We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/
#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics
Formal verification of axiom-free gödelian ontological argument and trinity necessity proof in Isabelle HOL. ~ Yong-Dock Kim. https://www.isa-afp.org/entries/Axiom_Free_Ontological_Trinity.html #IsabelleHOL #ITP
Do you want to do a PhD in Formal Methods and are interested in pursuing a PhD? Look no further, we have an open position leading to a joint degree from the University Paris-Sacly (France) and the University of Exeter (UK):
Information about the programme can be found at
* <https://www.exeter.ac.uk/study/pg-research/funding/phdfunding/paris-saclay/>
* <https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay>
All applications have to be made via the ADUM system:
<https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay>,
latest on the 22nd of March 2026.
#phd #phdposition #formal_logic #isabelleHOL #formal_mehods #joboffer #DiscreteMathematics #NumberSystems
Apply2Isar: Automatically converting Isabelle/HOL apply-style proofs to structured Isar. ~ Sage Binder, Hanna Lachnitt, Katherine Kosaian. https://arxiv.org/abs/2603.07771v1 #IsabelleHOL #ITP
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style scripts to declarative Isar. This allows users to write complex, possibly fragile apply-style scripts, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.
Readings shared February 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/25-readings_shared_02-24-26 #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire
