José A. AlonsoReadings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver
The HOL-Light library of multivariate real analysis in Rocq. ~ Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. https://inria.hal.science/hal-05464922/file/Reusing_HOLLight_library_in_Rocq-7.pdf #ITP #RocqProver #HOL_Light #Math
Candle: A verified implementation of HOL Light. ~ Oskar Abrahamsson et als. https://link.springer.com/article/10.1007/s10817-025-09743-8 #ITP #HOL4 #HOL_Light
Candle: A Verified Implementation of HOL Light (Extended Version) - Journal of Automated Reasoning
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
1000+ theorems (The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!). ~ Katja Berčič et als. https://1000-plus.github.io/all #Math #ITP #IsabelleHOL #HOL_Light #Rocq #LeanProver #Metamath #Mizar
Growing a modular framework for modal systems - HOLMS: a HOL Light library. ~ Antonella Bilotta. https://arxiv.org/abs/2506.10048 #ITP #HOL_Light #Logic #Math
Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an accessible introduction to the library, the fundamentals of modal logic are outlined first, followed by a concise manual for the proof assistant itself. The core contribution of this work on HOLMS is the development of a unified and modular strategy for proving adequacy theorems with respect to relational semantics directly within HOL Light for several normal modal systems, currently including K, T, K4, and GL. Adequacy theorems establish a formal connection between syntactic proof systems and their intended relational models, ensuring that derivable statements align with valid ones. This approach extends previous research on Gödel-Löb logic (GL) by two HOLMS developers. It also assesses the generality and compositionality of the completeness proofs in George Boolos' monograph \textit{The logic of provability}. Beyond theoretical contributions, HOLMS incorporates automated decision procedures and a countermodel constructor for K, T, K4, and GL, illustrating how general-purpose proof assistants can be effectively combined with research on labelled sequent calculi and key insights from correspondence and bisimulation theories. The implementation in HOL Light demonstrates the feasibility of mechanising modal reasoning in a flexible and robust manner, paving the way for further developments of the HOLMS framework.
A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874 #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
Readings shared January 26, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/26-readings_shared_01-26-25 #ITP #LeanProver #HOL_Light #Math
