Readings shared January 24, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver
0
1
0
0
Hashtag
#HOL_Light
Advertisement · 728 × 90
Candle: A verified implementation of HOL Light. ~ Oskar Abrahamsson et als. link.springer.com/article/10.1... #ITP #HOL4 #HOL_Light
1
0
0
0
Readings shared October 29, 2025. jaalonso.github.io/vestigium/po... #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq
0
0
0
0
1000+ theorems (The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!). ~ Katja Berčič et als. 1000-plus.github.io/all #Math #ITP #IsabelleHOL #HOL_Light #Rocq #LeanProver #Metamath #Mizar
3
2
0
0
Readings shared June 13, 2025. jaalonso.github.io/vestigium/po... #AI #AIforMath #Autoformalization #CoqProver #HOL_Light #ITP #IsabelleHOL #LLMs #LeanProver #Logic #MLLMs #Math #Rocq
0
0
0
0
Growing a modular framework for modal systems - HOLMS: a HOL Light library. ~ Antonella Bilotta. arxiv.org/abs/2506.10048 #ITP #HOL_Light #Logic #Math
2
0
0
0
Readings shared March 23, 2025. jaalonso.github.io/vestigium/po... #Agda #Coq #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #SetTheory
0
0
0
0
A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. ieeexplore.ieee.org/stamp/stamp.... #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
2
1
0
0
Readings shared January 26, 2025. jaalonso.github.io/vestigium/po... #ITP #LeanProver #HOL_Light #Math
0
0
0
0
Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. hvg.ece.concordia.ca/Publications... #ITP #HOL_Light #Math
2
0
0
0
Readings shared January 4, 2025. jaalonso.github.io/vestigium/po... #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python
1
0
0
0
Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. overlay.uniud.it/workshop/202... #ITP #HOL_Light #Logic
0
0
0
0
Readings shared September 28, 2024. jaalonso.github.io/vestigium/po... #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math
0
0
0
0
Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid & Sofiène Tahar. hvg.ece.concordia.ca/projects/fvp... #ITP #HOL_Light
0
0
0
0
Readings shared September 14, 2024. jaalonso.github.io/vestigium/po... #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs
0
1
0
0
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. www.amazon.science/blog/better-... #ITP #HOL_Light
1
0
0
0
Lecturas compartidas el 25 de junio de 2024. jaalonso.github.io/vestigium/po... #ITP #Agda #Coq #HOL #HOL_Light #IsabelleHOL #Lean4 #Metamath #Math #Haskell #Python #Algorithms #AI #MachineLearning
0
0
0
0
0
0
0
0
0
0
0
0
Lecturas compartidas el 6 de junio de 2024. jaalonso.github.io/vestigium/po... #ITP #Lean4 #IsabelleHOL #HOL_Light #Math
0
0
0
0
The HOL Light library of formalized mathematics. ~ Marco Maggesi. europroofnet.github.io/_pages/WG4/S... #ITP #HOL_Light #Math
0
0
0
0
Lecturas compartidas el 30 de mayo de 2024. jaalonso.github.io/vestigium/po... #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
0
0
0
0
Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. easychair.org/publications... #ITP #HOL_Light #Coq
0
0
0
0
Lecturas compartidas el 11 de mayo de 2024. jalonso.substack.com/lecturas-com... #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
0
0
0
0
Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. arxiv.org/abs/2405.04699 #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math
2
0
0
0
Lecturas compartidas el 8 de mayo de 2024. jalonso.substack.com/lecturas-com... #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math
0
0
0
0
Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. files.inria.fr/blanqui/lpar... #ITP #HOL_Light #Coq
1
0
0
0
Lecturas compartidas el 28 de abril de 2024. jalonso.substack.com/lecturas-com... #ITP #Lean4 #IsabelleHOL #HOL_Light #Math
0
0
0
0
Formalization of the telegrapher’s equations using higher-order-logic theorem proving. ~ Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar. www.researchgate.net/profile/Adna... #ITP #HOL_Light #Math
0
0
0
0