José A. Alonso @Jose_A_Alonso@mathstodon.xyz4/11/2025, 6:29:15 AMPublicReadings shared April 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/10-readings_shared_04-10-25 #AI #ATP #CommonLisp #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Programming #ReasoningReadings shared April 10, 2025The readings shared in Bluesky on 10 April 2025 are Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. #ITP #LeanProver #Math Formalization of gyrovector spaces as modelsjaalonso.github.io · Vestigium