The preceding Etats de la recherche on this topic happened in Rennes, 2006, and the organizers of the present edition asked me to make the bridge between these two sessions. My 2006 talks were devoted to the theory of heights and equidistribution theorems for algebraic dynamical systems. I will start from there by presenting the framework allowed by Arakelov geometry, and explaining the recent manuscript of X. Yuan and S.-W. Zhang who provide a birational perspective to these concepts. The theory is a bit complex and technical but I will try to emphasize the parallel between those ideas and the ones that lie at the ground of pluripotential theory in complex analysis, or in the theory of b-divisors in algebraic geometry.[-]

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.[-]