A formally verified proof of the Central Limit Theorem

TL;DR

This paper presents a formally verified proof of the Central Limit Theorem using the Isabelle proof assistant, extending existing libraries and demonstrating the convergence of sums of random variables to the normal distribution.

Contribution

It provides the first formal proof of the CLT in Isabelle, enhancing the proof assistant's libraries for analysis and probability.

Findings

Successful formal verification of the CLT in Isabelle

Extension of Isabelle's libraries for measure-theoretic probability

Insights into formalization process and lessons learned

Abstract

We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.