Mechanised Mathematics

Picture of Michael  Norrish Michael Norrish

9 Feb 2023

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.

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