The first Janko group J_1: simplicity and formalization
Summary
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.