The readings shared in Bluesky on 3 February 2025 are

• A comprehensive survey of the Lean 4 theorem prover: Architecture, applications, and advances. ~ Xichen Tang. #ITP #LeanProver
• Differential privacy (in Isabelle/HOL). ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• Differential privacy using quasi-Borel spaces. ~ Michikazu Hirata. #ITP #IsabelleHOL
• Maxima in the browser using Embedded Common Lisp on WASM. #Maxima #CoomonLisp #Math
• #Exercitium: La bandera tricolor. #Haskell #Python #CommonLisp