The readings shared in Bluesky on 16 June 2025 are

• A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van De Velde, Andrew Yang. #ITP #LeanProver #Math
• LeanExplore: A search engine for Lean 4 declarations. ~ Justin Asher. #ITP #LeanProver
• An approach to formalize information-theoretic security of multiparty computation protocols. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Rocq
• Toward a formalization of secure multiparty computation stack. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikaaw. #ITP #CoqProver #Rocq