José A. AlonsoSep 24
Readings shared September 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/24-readings_shared_09-23-25 #Abella #Agda #CategoryTheory #CoqProver #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Naproche #Rocq #RustLang
Readings shared September 23, 2025

The readings shared in Bluesky on 23 September 2025 are: Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math A formal analysis of algorithms for m

Vestigium
José A. AlonsoSep 23
A natural language formalization of perfectoid rings in ℕaproche. ~ Peter Koepke. https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.6/LIPIcs.ITP.2025.6.pdf #ITP #Naproche #Math