Verifying large correctness proofs in proof assistants

The current outline of the project, is based around 3 pillars namely:

- Formal verification of mathematics which is often done through proof assistants software the most popular being a language called lean. - Automated reasoning, where we try to automate aspects of generating mathematical proofs.

- And proof mining, which is the process of unwinding mathematical proofs using techniques/results in the field of proof mining to generate new results.

All 3 of these pillars are interconnected. In the area of proof mining there has been great success in using convergence proofs in real analysis and ergodic theory to generate rates of convergence or rates of metastability. Here at Bath the mathfound research group has been very successful in generating similar results relating to convergence in probability theory. The hope of this project is to continue that success through further exploration and research.

As I mentioned before all 3 of these pillars are interconnected, so work in one often spirals in to working in the others. Because of this, the outline of the project is to join the ongoing research in proof mining in probability theory with the prospect of the research spiralling into 1 or more of the 3 pillars outlined above.