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