Appears in collection : Lean for the curious mathematician / Lean pour mathématiciens

This talk has a dual aim: to provide a mathematical overview of Stone duality theory, and to invite collaboration on its Lean formalization. Stone duality is an algebraic way of looking at profinite topologies. A profinite set is a compact, T2, totally disconnected space, or, equivalently, a topological space which can be obtained as the projective limit of finite discrete spaces. Stone proved in the 1930s that the category of profinite sets is dually equivalent to that of Boolean algebras, and, more generally, that the category of spectral spaces is dually equivalent to that of bounded distributive lattices. I will explain how spectral spaces can be advantageously understood as profinite posets, also known as Priestley spaces. I will also point to more modern research that takes Stone duality further, and may touch upon some mathematical contexts where it pops up, notably topos theory and condensed mathematics. Elements of Stone duality theory have been formalized in Lean over the past few years, and I will report on some of the most recent progress. I will also propose a number of concrete formalization goals at various levels of estimated difficulty, to provide the audience with some potential project ideas for this week.