The readings shared in Bluesky on 26 January 2025 are

• Readings shared January 25, 2025. #ITP #Agda #Coq #Rocq #IsabelleHOL #Math #FunctionalProgramming #Haskell #JuliaLang
• Certified knowledge compilation with application to formally verified model counting. ~ Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule. #ITP #LeanProver
• Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. #ITP #HOL_Light #Math
• Math Encounters: "You want proof? I'll give you proof! (Mathematical arguments from Euclid to Lean)". ~ Jeremy Avigad. #ITP #LeanProver #Math