My research involves using the Interactive Theorem Prover, Isabelle/HOL, to formalise matching algorithms. Using a theorem prover allows you to provide formal guarantees about the efficacy of an algorithm. The focus of my research is on matching algorithms used in social welfare schemes where people’s livelihood is at stake. Without these formal guarantees, it is possible that lives are being lost unnecessarily in social welfare schemes through inefficiencies in the underlying algorithms. My other areas of interest include formalising mathematics, in particular problems relating to Green’s Theorem.
I chose to pursue a PhD with STAI CDT as it is a great way to learn more about the context of my research in the field of safe and trusted AI through the seminars and masterclasses. I also appreciate the cohort-based approach as I enjoy discussing with my peers about STAI topics and hearing their unique perspectives.
–
Master’s Qualification: MMath in Mathematics, University of Warwick
