Keywords: Probability Theory, HOL4, Interactive Theorem Proving, Proof Mechanisation
Units: 12/24 units
Background
Mechanising mathematics is the task of turning (relatively) wellunderstood mathematics into verified proofs with an interactive theoremproving system. Such verified material can then lie behind highassurance software.
This project is an opportunity for students who wants to learn the HOL4 theoremproving 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 develop a formal version of the Theory of Martingale of probability theory (and stochastic process). This will include the following tasks:

Extend the existing mechanisation of HOL4’s formal probability library (in which martingale has already been defined with a small set of lemmas), up to some Martingale Convergence Theorems necessary for the proof of SLLN (see below);

Use Martingale Convergence Theorems to prove the Strong Laws of Large Numbers (SLLN) for I.I.D. random variables (independent with identical distributions). (Informal proofs can be found in Chapter 2324 of [Schilling] or Chapter 1718 of [Schilling1])

(for 24 credits) Selected advanced topics and application of martingale methods to practical problems (following mainly Chapter 7 of [Shiryaev2]).
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
 [Schilling] Schilling, R.L.: Measures, Integrals and Martingales (2nd Edition). Cambridge University Press (2017).
 [Schilling1] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge University Press (2005).
 [Shiryaev2] Shiryaev, A.N.: Probability2. Springer, New York, NY (2019). doi:10.1007/9780387722085
Requirements:
Basic knowledge of formal logic and lambdacalculus (simple typed); some experiences with interactive theorem provers; mathematics (calculus and elementary probability theory)