Formalisation of the Finite Simple Conway Groups in Lean
Publication date
Authors
DOI
Document Type
Bachelor Thesis
Metadata
Show full item recordCollections
License
CC-BY-NC-ND
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.