Readings shared July 16, 2025
The readings shared in Bluesky on 16 July 2025 are
- Formalization of derived categories in Lean/Mathlib. ~ Joël Riou. #ITP #LeanProver #Math
- Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
- A complete formalization of Fermat’s Last Theorem for regular primes in Lean. ~ Alex J. Best et als. #ITP #LeanProver #Math
- Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
- A simple formalization of alpha-equivalence. ~ Kalmer Apinis, Danel Ahman. #ITP #Rocq
- Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #CoqProver
- LISA: A modern proof system. ~ Simon Guilloud, Sankalp Gambhir, Viktor Kunčak. #ITP #Lisa #Math
- #Exercitium: Problemas de programación con Haskell de febrero de 2021. #Haskell #FunctionalProgramming