José A. Alonso @Jose_A_Alonso@mathstodon.xyz6/22/2025, 3:29:37 PMPublicReadings shared June 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/22-readings_shared_06-21-25 #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #PrologReadings shared June 21, 2025The readings shared in Bluesky on 21 June 2025 are Theorem proving in Lean 4. ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich et als. #ITP #LeanProver Certifying projected knowledgjaalonso.github.io · Vestigium