José A. Alonso @Jose_A_Alonso@mathstodon.xyz9/18/2025, 7:19:53 AMPublicReadings shared September 17, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/18-readings_shared_09-17-25 #AI #Autoformalization #CAS #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Macaulay2 #Math #Mathlib #Physics #Rocq #SMTReadings shared September 17, 2025The readings shared in Bluesky on 17 September 2025 are: Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin, Colin Jones, John Velkey, Tyler R. Josephson. #ITP #LeanPjaalonso.github.io · Vestigium