The readings shared in Bluesky on 23 November 2025 are:

• DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof
• Verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda
• Formalization of derived categories in Lean/mathlib. ~ Joël Riou. #ITP #LeanProver
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver
• 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
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• Testing a priority queue with Monolith. ~ François Pottier. #OCaml #FunctionalProgramming
• Reseña de «DeepMind’s latest: An AI for handling mathematical proofs». #AI #Math #ITP #LeanProver #AlphaProof