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 idea is an opportunity for a student to learn the HOL4 theorem-proving system and realise their choice of mathematics. At thesis levels (PhD or Masters), 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.