Formalisation of the Finite Simple Conway Groups in Lean

Abstract

Study of the Conway groups, a family of sporadic simple groups closely related to the Leech lattice. We will demonstrate a construction of the Leech lattice, show how it can be used to construct the Conway groups and provide a proof of the simplicity of one of them, Co1. Furthermore, we formalise part of this proof in the Lean theorem prover.