Keywords: Probability Theory, HOL4, Interactive Theorem Proving, Proof Mechanisation
Units: 12/24 units
Background
Mechanising mathematics is the task of turning (relatively) well-understood mathematics into verified proofs with an interactive theorem-proving system. Such verified material can then lie behind high-assurance software.
This project is an opportunity for students who wants to learn the HOL4 theorem-proving system and realise an important piece of mathematics. At thesis level (24 units), the simple mechanisation of the mathematics would need to be augmented with an application of the mechanisation and/or significant novelty in the nature of the proofs.
Research Questions and Tasks
The aim of this research project is to mechanize the informal proofs of various versions of the Central Limit Theorems (CLT) in Probability Theory. This will include the following tasks:
-
Extend the existing mechanisation of HOL4’s formal probability library to cover “convergence (of random sequences) in distribution” with various alternative definitions and supporting lemmas.
-
Add the theory of random variables with normal distributions by porting the existing (old) work done by Concordia HVG people.
-
Prove CLT for I.I.D. random variables (independent with identical distributions).
-
(for 24 credits) Mechanize Liapounov’s form of the CLT (i.e. independent with bounded third moments) by Lindeberg’s method (or by characteristic functions, which requires more preparations).
The development should follow modern techniques and guidelines for HOL4, e.g. [HOLTutorial] and [HOL4]. Ideally, the project will be submitted to HOL4 official as part of its core theories.
NOTE: The student will get some basic training through a mini course to get familar with interactive theorem proving (ITP) techniques (and HOL4 in particular).
References
- [HOLTutorial] The HOL System LOGIC
- [HOL4] The HOL System DESCRIPTION
- [Chung] Chung, K.L.: A Course in Probability Theory. Academic Press (2001).
- [Shiryaev1] Shiryaev, A.N.: Probability-1. Springer-Verlag New York, New York, NY (2016).
Requirements:
Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; mathematics (calculus and elementary probability theory)