"I recommend meeting your potential supervisor before committing, especially if you have the chance to do a research project with them." Image My PhD is concerned with formalising mathematical proofs with the aid of the proof assistant Isabelle which checks that the proof is correct and supplies small steps in the proof. This has some unique challenges: it requires creativity to express definitions precisely and careful thought to fit all the different parts of the proof together. The benefit is that it provides a complete understanding of all the nuances of a proof or concept which could not be fully understood in any other way. My project aims to formalise geometric algebra and use my formalisation to express an intrinsic definition of manifolds. This would provide a useful reference for mathematicians and physicists as well as extending the boundaries of formalised mathematics. However, I am still in my first year, so there may be some surprises about where this leads me. Why AIAI? I completed my final year undergraduate project with Jacques Fleuriot, who is now my PhD supervisor. This gave me familiarity with the area of interactive theorem proving which I loved because I felt it was more rigourous and gave deeper insight than other ways of looking at mathematics. I also found that Jacques was a great person to work with because he is both knowledgeable and enthusiastic. These were the two main reasons I wanted to do a P hD in AIAI. Advice for other PhD applicants I recommend meeting your potential supervisor before committing, especially if you have the chance to do a research project with them. From talking to other PhD students, it seems to make a big difference if your supervisor is someone whom you work well with and who gives you the right kind of support. This article was published on 2024-11-22
