#isabellehol — Public Fediverse posts

Mechanizing typed regulatory actions for security tokens: semantics, falsification, and bounded EVM evidence. ~ Jinwook Kim. https://arxiv.org/abs/2608.29134v2 #IsabelleHOL #ITP

Readings shared July 22, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/06-readings_shared_07-06-26 #AI4Math #Agda #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #PVS

Readings shared May 9, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/10-readings_shared_05-09-26 #AI4Math #ATP #Aristotle #CompSci #CoqProver #FunctionalProgramming #Haskell #History #ITP #IsabelleHOL #LeanProver #Logic #Math #Mizar #Ocaml #RocqProver

Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared January 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/15-readings_shared_01-14-26 #AI #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver

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

Curso "Razonamiento automático (2017-18)". https://jaalonso.github.io/cursos/m-ra-17 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2017-18)". https://jaalonso.github.io/cursos/m-ra-17 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2016-17)". https://jaalonso.github.io/cursos/m-ra-14 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2014-15)". https://jaalonso.github.io/cursos/m-ra-14 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2013-14)". https://jaalonso.github.io/cursos/m-ra-13 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2012-13)". https://jaalonso.github.io/cursos/m-ra-12 #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2011-12)". https://jaalonso.github.io/cursos/m-ra-11 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2008-09)". https://jaalonso.github.io/cursos/d-ra-08 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

Curso "Razonamiento automático (2007-08)". https://jaalonso.github.io/cursos/d-ra-07 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL