Proved Algorithms in Geometric Group Theory

Abstract

In the recent decades, computers have opened up novel ways of doing mathematics. The speed and raw power of computers has been used to perform searches over previously untractable spaces of objects and proofs, and complementarily, the ability of computers be systematic and methodical has been utilised to formalise and automatically verify complicated proofs. Although writing programs and constructing proofs seem like different activities, in type-theoretic foundations of mathematics these can both be seen as instances of constructing a term of a type. Proof assistants based on dependent type theory leverage this correspondence to serve both as theorem provers as well as functional programming languages. As programming and proving can be done within the same framework of dependent type theory, computers searches can in principle be augmented with proofs to give "proved algorithms" that have been proved to be correct and returns results together with formal proofs when run. Geometric group theory is a relatively new area that is at the intersection of algebra and topology, and connected to several others. Over the last few years, there have been some significant results in the area achieved with the help of computer searches. This thesis is centered on the theme of “Proved Algorithms in Geometric Group Theory”, using the Lean4 theorem prover and programming language to formally prove results in geometric group theory involving a mix of proofs and computations.