Mechanised Probability Theory - Ergodic Theory

Picture of Chun Tian

10 Oct 2023

Keywords: Probability Theory, HOL4, Interactive Theorem Proving, Proof Mechanisation
Units: 12 units


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 develop a formal version of the Theory of Stationary (Strict Sense) Random Sequences and Ergodic Theory. This will include the following tasks:

  • Starting with the existing mechanisation of HOL4’s formal probability library, adds the concepts and supporting theorems for measure-preserving transformations, ergodicity and eventually prove Birkhoff’s Ergodic Theorem. (Informal proofs can be found in Chapter 5 of [Shiryaev2], cf. also [Lindgren])

  • Uses the Ergodic Theorem to prove (again) the Strong Laws of Large Numbers (SLLN) for I.I.D. random variables (independent with identical distributions).

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



Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; mathematics (calculus and elementary probability theory)

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up