A formally verified proof of the central limit theorem

DOI10.1007/s10817-017-9404-xzbMath1425.68369arXiv1405.7012OpenAlexW2963637004MaRDI QIDQ1694568

Jeremy Avigad, Johannes Hölzl, Luke Serafin

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1405.7012

zbMATH Keywords

central limit theoremmeasure theoryinteractive theorem proving

Mathematics Subject Classification ID

Related Items (9)

Proving divide and conquer complexities in Isabelle/HOL ⋮ A heuristic prover for real inequalities ⋮ Computational logic: its origins and applications ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ A formally verified proof of the central limit theorem ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ A Formal Proof of Cauchy’s Residue Theorem

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Sledgehammer
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• A history of the central limit theorem. From classical to modern probability theory
• Isabelle/HOL. A proof assistant for higher-order logic
• A formally verified proof of the central limit theorem
• Formalization of Normal Random Variables in HOL
• The Flow of ODEs
• Formalization of real analysis: a survey of proof assistants and libraries
• Three Chapters of Measure Theory in Isabelle/HOL
• Formalization of Entropy Measures in HOL
• Type classes for efficient exact real arithmetic in Coq
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: A formally verified proof of the central limit theorem