1 Introduction

The aim of this document is to give a detailed proof of Stone duality for Boolean algebras [ 1 ] to facilitate its formalization in Mathlib. Note that Stone actually proved something more general for bounded distributive lattices [ 2 ] . (Below, I will cut everything into very small numbered lemmas and definitions which is not how I usually like to write math, but it seemed like it might be useful for organizing the formalization. TODO: put this in the lean blueprint format.)