#hol_light — Public Fediverse posts

Readings 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

Readings shared October 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/30-readings_shared_10-29-25 #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

Readings shared October 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/30-readings_shared_10-29-25 #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

Readings shared October 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/30-readings_shared_10-29-25 #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

Readings shared October 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/30-readings_shared_10-29-25 #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

Readings shared October 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/30-readings_shared_10-29-25 #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

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

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

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

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

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

Readings shared June 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/14-readings_shared_06-13-25 #AI #AIforMath #Autoformalization #CoqProver #HOL_Light #ITP #IsabelleHOL #LLMs #LeanProver #Logic #MLLMs #Math #Rocq

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

Readings shared March 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-23-25 #Agda #Coq #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #SetTheory

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

Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. https://hvg.ece.concordia.ca/Publications/Thesis/Elif-PhD-Thesis.pdf #ITP #HOL_Light #Math

Readings shared January 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/04-readings_shared_01-04-25 #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python

Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. https://overlay.uniud.it/workshop/2024/papers/paper5.pdf #ITP #HOL_Light #Logic

Readings shared September 28, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/28-readings_shared_09-28-24 #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math

Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid & Sofiène Tahar. https://hvg.ece.concordia.ca/projects/fvps/pde/Formal_Verification_of_Coupled_Transmission_Lines.pdf #ITP #HOL_Light

Readings shared September 14, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/14-readings_shared_09-14-24 #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs

Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. https://www.amazon.science/blog/better-performing-25519-elliptic-curve-cryptography #ITP #HOL_Light

Lecturas compartidas el 25 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/26-lecturas_compartidas_el_25-jun-24 #ITP #Agda #Coq #HOL #HOL_Light #IsabelleHOL #Lean4 #Metamath #Math #Haskell #Python #Algorithms #AI #MachineLearning

Even more on HOL Light (3). ~ Freek Wiedijk. https://youtu.be/R-3kPIHB2RA #ITP #HOL_Light

More on HOL Light (2). ~ Freek Wiedijk. https://youtu.be/ux96swHX-6s #ITP #HOL_Light

Lecturas compartidas el 6 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/07-lecturas_compartidas_el_06-jun-24 #ITP #Lean4 #IsabelleHOL #HOL_Light #Math

The HOL Light library of formalized mathematics. ~ Marco Maggesi. https://europroofnet.github.io/_pages/WG4/Sep22/maggesi.pdf #ITP #HOL_Light #Math

Lecturas compartidas el 30 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24 #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs

Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. https://easychair.org/publications/paper/mtFT #ITP #HOL_Light #Coq

Lecturas compartidas el 11 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-11-de-mayo #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp

Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. https://arxiv.org/abs/2405.04699 #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math

Lecturas compartidas el 8 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-8-de-mayo #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math

Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. https://files.inria.fr/blanqui/lpar24.pdf #ITP #HOL_Light #Coq

Lecturas compartidas el 28 de abril de 2024. https://jalonso.substack.com/lecturas-compartidas-el-28-de-abril #ITP #Lean4 #IsabelleHOL #HOL_Light #Math

Formalization of the telegrapher’s equations using higher-order-logic theorem proving. ~ Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar. https://www.researchgate.net/profile/Adnan-Rashid-7/publication/379913006_Formalization_of_the_Telegrapher's_Equations_using_Higher-Order-Logic_Theorem_Proving/links/6621a78239e7641c0bd77086/Formalization-of-the-Telegraphers-Equations-using-Higher-Order-Logic-Theorem-Proving.pdf #ITP #HOL_Light #Math