The readings shared in Bluesky on 19 May 2025 are

• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #LeanProver #Math
• Towards a mechanization of fraud proof games in Lean. ~ Martín Ceresa, César Sánchez. #ITP #LeanProver
• Farey sequences and Ford circles (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Formal verification of a fail-safe cross-chain bridge. ~ Filip Marić, Bernhard Scholz, Pavle Subotić. #ITP #IsabelleHOL
• Verifying smart contract transformations using bisimulations. ~ Kegan McIlwaine, James Caldwell. #ITP #IsabelleHOL
• Formally specifying contract optimizations with bisimulations in Coq. ~ Derek Sorensen. #ITP #Coq #Rocq
• Math for programming (Learn the math, write better code). ~ Ronald T. Kneusel. #Math #Python #Programming
• Lisp. But why? ~ Raj. #CommonLisp #Programming