Programs, data and certificates for: The automorphism group of an extremal [72,36,16] code is trivial

Supplementary files for the computer-assisted proofs in the paper "The automorphism group of an extremal [72,36,16] code is trivial" (doi:10.5281/zenodo.23789973). Abstract of the paper. Whether a binary doubly-even self-dual [72,36,16] code exists is a question raised by Sloane in 1973. A series of papers, surveyed by Borello, shows that the automorphism group of such a code is trivial or isomorphic to C2, C3, C2 × C2 or C5. We prove that such a code has no automorphism of order 2, 3 or 5, and hence no nontrivial automorphism. Each such automorphism reduces the problem to a finite computer search. For order 2 the search runs over symmetric bilinear forms on the 41 self-dual [36,18,8] codes. An automorphism of order 3 leads to a search over labellings of the Hermitian self-dual [24,12,8] codes over F4 by the extended Golay code. Order 5 reduces to 7 × 7 unitary matrices over F16. Along the way we classify the Hermitian self-dual [24,12,8] codes over F4: there are 26 924 931 of them up to monomial equivalence. The archive contains, for each search, the programs and the logs of its runs, and the input files of the searches of orders 2 and 3. It also contains the two programs that classify the Hermitian self-dual [24,12,8] codes over F4 and the resulting list of 13 485 816 classes up to monomial equivalence and conjugation: one class for each self-conjugate code counted in the abstract and one for each pair of conjugate codes. The archive also holds the outputs of the checks described in the paper, among them the runs of a second implementation of each search of orders 3 and 5 and of an independent program for five of the 41 searches of order 2. For each of the 41 searches of order 2, parts of the search were rerun, and a separate check confirms that the runs cover the whole search. A smaller computation that excludes subgroups C2 × C2 directly is included as a further check of this case, which the searches of order 2 also exclude. The archive also contains a Lean formalization of the reductions. The programs are written in C and Python 3, and README_v2.md describes the files and how to use them.