A Formally Verified Proof of the Central Limit Theorem

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 o...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2017-12, Vol.59 (4), p.389-423
Main Authors: Avigad, Jeremy, Hölzl, Johannes, Serafin, Luke
Format: Article
Language:English
Subjects:
Artificial Intelligence
Central limit theorem
Characteristic functions
Computer Science
Fourier transforms
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Normal distribution
Probability distribution functions
Random variables
Statistical analysis
Symbolic and Algebraic Manipulation
Theorem proving
Theorems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-017-9404-x