Machine Proofs for Adams Differentials and Extension Problems among CW Spectra
Weinan Lin, Guozhen Wang, Zhouli Xu
TL;DR
The paper presents a computational framework for generating Adams spectral sequence data and machine-generated proofs for CW spectra, enabling systematic discovery of Adams $d_2$-differentials and extensions. By computing $E_2$-pages, inter-page maps, and extension data with automated proofs, and by releasing a transparent dataset and an extensive Table of Proofs, the authors contribute to resolving aspects of the Last Kervaire Invariant Problem in dimension $126$. The work leverages the Generalized Leibniz Rule and the Generalized Mahowald Trick to derive new differentials and extensions, augmented by human insight, and provides navigable charts to interpret outputs. Overall, this approach advances computational homotopy theory by offering reproducible, publicly accessible proofs and data for complex spectral-sequence calculations.
Abstract
In this document, we describe the process of obtaining numerous Adams differentials and extensions using computational methods, as well as how to interpret the dataset uploaded to Zenodo. Detailed proofs of the machine-generated results are also provided. The dataset includes information on 49 CW spectra, 180 maps, and 61 cofiber sequences. Leveraging these results, and with the addition of some ad hoc arguments derived through human insight, we successfully resolved the Last Kervaire Invariant Problem in dimension 126.