The uniqueness of groups of type \(J_ 4\) (Q1177418)

From the introduction of the authors: ``We give the first computer free proof of the uniqueness of groups of type \(J_ 4\). In addition we supply simplified proofs of some properties of such groups, such as the structure of certain subgroups.\dots Around 1980, Norton, Parker, and Thackray proved the existence and uniqueness of groups of type \(J_ 4\) using extensive machine computation.\dots Norton et al. constructed \(J_ 4\) as a linear group in 112 dimensions over the field of order 2. While the notion of a 2-local geometry did not exist at that time, this geometry plays an implicit role\dots'' The authors' proof is based on the theory of so called uniqueness systems presented by them in a forthcoming paper. This theory is then applied to the 2-local geometry of a group \(G\) of type \(J_ 4\) and its collinearity graph. The main step in the uniqueness proof is to show that the graph is simply connected. Here, a group of type \(J_ 4\) is a simple group as (discovered and) described by Zvonimir Janko in 1976.