## 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:
- 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.