Proofs are an important part of mathematics, but they are not without their flaws. Most proofs are written by humans, and humans make mistakes. In this thesis, we explore the use of proof assistants to construct formal ...