This document is a blueprint for the formalization of the central limit theorem in Lean. For the proof, we will introduce and use characteristic functions, as well as the notion of tightness of sets of measures.

The main references for the results detailed here are

• chapter 6 of Foundations of Modern Probability (3rd ed.), by Olav Kallenberg,

• chapter 8 of Measure Theory, volume II, by V. Bogachev.

• chapter 3 of Markov Processes, Characterization and Convergence, by S.N. Ethier and T.G. Kurtz.

This blueprint is maintained by Rémy Degenne. Part of the proof is inspired by a document written by Peter Pfaffelhuber, in particular the use in the proof of the separating sigma-algebra of exponential polynomials as in the book by Ethier and Kurtz.