The first Janko group J_1: simplicity and formalization

Abstract

In this thesis, we will examine the first Janko group J_1. It is a sporadic group, which means that it is a finite and simple group. The main goal of this thesis is to prove the simplicity of a finite group that contains an involution i such that the centralizer of i is isomorphic to ⟨i⟩ × A_5, that has no subgroups of index 2 and in which all Sylow 2-subgroups are abelian. As it turns out, the group J_1 satisfies these properties. Although the theorem has already been given and proven by Zvonimir Janko in 1965, we give an extensive and complete proof, which leaves few gaps for the reader to fill. Parts of the proof of the theorem will also be formalized in the proof assistant Lean. We want to emphasize that we will not prove that J_1 does possess the properties of the theorem in this thesis; we will only prove that groups that do satisfy them, are simple.