Sam's formalization corner

I sometimes contribute to the formalization of mathematics in computer systems such as Coq/Rocq and Lean. I list my main contributions here.

• Draft: Stone duality in Lean, with Dagur Asgeirsson, Tomas Jakl, and Filippo A.E. Nuccio. Work started at Lean for the curious mathematician 2024. Parts of this work that have been added to Mathlib so far:
• May 2024: feat(Mathlib/Order/PrimeSeparator): prime ideal separator in a bounded distributive lattice.
• May 2024: feat(Mathlib/Order/Ideal): ideals of sets are stable under directed unions and chains.
• February 2024: a Uniform Interpolation Calculator for intuitionistic propositional logic, modal logics K and GL, and intuitionistic Strong Löb logic iSL. This is based on our verified Coq implementation of the underlying theorems, joint work with Hugo Férée, Iris van der Giessen, and Ian Shillito, with further contributions by Yago Iglesias Vazquez.
• October 2023: feat: Adjunction between topological spaces and locales, with Anne Baanen, Leopold Mayer, and Brendan Seamas Murphy, started at the Banff workshop on Formalization of cohomology theories.
• July 2022: feat(algebraic_geometry): comap of surjective homomorphism is closed embedding, with Jake Levinson, work done at Lean for the curious mathematician 2022.