Machine Proofs for Adams Differentials and Extension Problems among CW Spectra

Guozhen Wang; Weinan Lin; Zhouli Xu

REVIEW 5 major objections 8 minor 1 cited by

Machine Proofs for Adams Differentials and Extension Problems among CW Spectra

T0 review · 5 major / 8 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Machine-generated, checkable proofs of Adams differentials and extensions, with a few human arguments, resolve the Last Kervaire Invariant Problem in dimension 126.

desk verdict A big, honest computational dataset for Adams spectral sequences; it deserves a serious referee, but acceptance should be tied to clarifying its dependency on the companion paper. read the letter →

arxiv 2412.10876 v2 pith:BJ5GUP4F submitted 2024-12-14 math.AT math.GN

Weinan Lin , Guozhen Wang , Zhouli Xu This is my paper · ORCID

classification math.ATmath.GN MSC 55T1555Q4555P42

keywords AdamsspectralsequencedifferentialsextensionproblemsCWspectraKervaireinvariantproblemmachine-generatedproofstablehomotopygroupsofspheresdata

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper is the computational companion to a solution of a long-standing stable homotopy problem: it presents the dataset and machine-generated proofs behind the resolution of the Last Kervaire Invariant Problem in dimension 126. The dataset covers 49 connective CW spectra, 180 maps between them, and 61 cofiber sequences, with Adams $E_2$ pages, $d_2$ differentials, higher differentials, and extensions computed by two programs. The central claim is that every computed Adams differential and extension in the dataset carries a machine-generated proof, organized in a searchable Table of Proofs, and that these results, together with a few hand-added differentials, close the dimension-126 case. A reader should care because the claims are not left as black-box computer output: each differential is documented as a nested case analysis that a reader can inspect row by row.

What carries the argument

The engine is the program ./ss, which stores an Adams spectral sequence as nested subgroups $0 = B_1^{s,t} \subseteq B_2^{s,t} \subseteq \cdots \subseteq Z_2^{s,t} \subseteq E_2^{s,t}$ and treats each differential as an isomorphism between quotient groups, storing both $d_r$ and its inverse $d_r^{-1}$. The same data structure is applied to a cofiber sequence $X \to Y \to Z$ to encode extensions as maps between filtration subgroups, so extensions become differential-like objects with their own filtration jump and source and target degrees. From the $d_2$ differentials computed by the program ./Adams, the program derives new differentials and extensions using the Leibniz rule, naturality, and two theorems from the companion paper - the generalized Leibniz rule and the generalized Mahowald trick - which give conditions under which auxiliary differentials or a cofiber sequence force the value of a target differential. Every step is recorded as a row in the Table of Proofs, with reason labels 'T' for a trial assumption and 'D' for the deduction that rules out candidates.

What would settle it

An independent recomputation of the Adams spectral sequence of $S^0$ in stems 122-127 and of $S^0/\nu$ in stem 126 would falsify the central claim if any listed $d_r$ value has a different target, or if a 'Try' row that is supposed to end in contradiction instead propagates consistently; equivalently, checking the machine proofs of the three hand-added differentials would reveal whether the Table of Proofs uses them only where the paper says.

Watch

Extended reading notes

Core claim

The paper's central claim is that the Adams spectral sequence data for a carefully chosen collection of CW spectra can be produced by machine together with machine-readable proofs of every computed differential and extension. The programs compute the $d_2$ differentials from secondary Steenrod operations, then derive all higher differentials and extensions by propagating through the Leibniz rule, naturality, and the generalized inference rules introduced in the companion paper. The proof of each nontrivial differential is a nested case analysis recorded in the Table of Proofs: candidate values are assumed one by one, each assumption is propagated until it contradicts an earlier computation or degree bound, and the candidate that survives is the value the machine records. Three differentials are put in by hand - two from the image of $J$ and one from power operations on $\mathrm{tmf}$ - and these are the only non-machine inputs. On top of this computed data, a few ad hoc human arguments complete the argument that resolves the Last Kervaire Invariant Problem in dimension 126.

Load-bearing premise

The whole edifice rests on the correctness of the two theorems imported from the companion paper, on the correctness of the implementations of the two programs, and on the assumption that every visible nontrivial differential in the data has length shorter than 1000; this document supplies no independent proof of any of those.

Editorial extensions

If this is right

If the companion paper's human arguments hold, the Last Kervaire Invariant Problem in dimension 126 is closed.
Every differential and extension in the dataset can be audited row by row, so the computational portion of the solution is not a black box.
The same pipeline - $d_2$ via secondary Steenrod operations followed by the generalized inference rules - can be applied to other connective CW spectra to produce $E_2$ pages, differentials, extensions, and proofs over a large stem range.
Encoding differentials as isomorphisms between nested quotient groups gives a uniform, memory-efficient way to organize and share spectral sequence computations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Run the same machinery on a spectrum outside the current list, such as a longer stunted real projective space, and compare the computed differentials with known stable homotopy groups; agreement would test the two generalized rules.
The Table of Proofs is a structured collection of case analyses, so an independent proof checker could turn each machine proof into a formally verified certificate.
Extending the computation to higher stems would test the length-shorter-than-1000 assumption directly; a longer visible differential would require revising the display convention.
The same nested proof format could be carried over to other spectral sequences once analogues of the generalized Leibniz rule and generalized Mahowald trick are established there.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

What you should know: this is a companion resource paper, and it is genuinely useful. The new thing is the scale: 49 CW spectra, 180 maps, 61 cofiber sequences, and a 21-million-row Table of Proofs recording machine-generated Adams differentials and extensions. That is not a rehash of earlier computations; no public dataset of this size for Adams spectral sequences exists. The paper is also unusually candid. It marks [NULL] entries, labels some differentials as undetermined with '?', and explicitly says which rows come from human-inserted facts, like the image-of-J differentials and the Bruner–Rognes tmf differential. That honesty matters, and it makes the resource usable.

The proof format is real work, not a black box: each row states the spectrum, bidegree, differential, and the reason (d2, naturality, Leibniz, Try/Deduction). The d2 rows are tied to secondary Steenrod operations with published references. If you want to check a particular differential, you can query proofs.db and trace the reason chain. That is a serious contribution.

The soft spots are real but not disqualifying. The proofs rely on the Generalized Leibniz Rule and Generalized Mahowald Trick from the authors' companion paper [7], and this document does not state those theorems or their hypotheses. So the Table of Proofs is not self-contained. A skeptical reader cannot verify the highest-risk rows (reason Syn, SynCs, SynIn) from this PDF alone. The stress-test worry about circularity does not actually land based on the text: nothing here shows that [7] proves its theorems using the very differentials that ./ss derives from them. But the paper should explicitly rule that out, ideally with a dependency diagram or a sentence in [7] confirming independence. Also, the assumption that all visible nontrivial differentials have length below 1000 is a computational truncation, not a theorem; it is stated, not justified. For the Kervaire range that may be harmless, but as written it is an open loop. And the programs ./Adams and ./ss are not formally verified; these are machine-generated proofs, not Lean/Coq-checked proofs. That is a limitation, not a fatal one.

Who is this for? Stable homotopy theorists working with Adams spectral sequences, and anyone who needs to rely on the Kervaire resolution in [7]. It should be peer-reviewed, but the referee should have access to both papers and should check whether the companion theorems are independent of the dataset. Conditional acceptance with a request for an explicit independence statement would be a fair outcome.

My own view: treat the dataset as a large computational resource with honest caveats, not as a closed formal proof. Send it to a serious referee.

Referee Report

5 major / 8 minor

Summary. The paper describes a computational dataset of Adams E2-pages, d2 differentials, Adams differentials, and extension data for 49 CW spectra, 180 maps, and 61 cofiber sequences, together with a 21-million-row Table of Proofs generated by the programs ./Adams and ./ss. The text specifies the data formats, the naming conventions for spectra and maps, the encoding of spectral sequence differentials, and the structure of the machine-generated proofs. Section 5 displays machine-generated Adams differentials for the sphere spectrum in stems 122–127 and for S0/nu in stem 126. The abstract states that these results, with additional human ad hoc arguments, resolve the Last Kervaire Invariant Problem in dimension 126; that solution is the subject of the companion paper [7]. The present document is therefore primarily a data paper and proof-log guide, but it also advertises a major mathematical outcome.

Significance. If the dataset and proof logs are sound, this is a valuable and unusually transparent computational resource for the Adams spectral sequence, with per-differential proof records and public data on Zenodo and GitHub. The paper also represents a concrete step toward a machine-assisted resolution of the Kervaire invariant problem in dimension 126, which would be a landmark result. The strengths include the reproducibility of the data artifacts and the explicit documentation of proof structures. However, the significance is conditional on two unresolved points: the correctness of the unverified programs that produced the proofs, and the independence of the companion-paper theorems used as inference rules. As written, the machine proofs are not independently auditable in a formal sense, and the possible circularity with [7] is not addressed. These concerns are load-bearing because the advertised Kervaire conclusion depends on the reliability of specific differential rows.

major comments (5)

[§1, §4 (reason='Syn', 'SynCs', 'SynIn')] The machine proofs invoke the Generalized Leibniz Rule and the Generalized Mahowald Trick from the companion paper [7], but this document neither states these theorems nor their hypotheses, and it does not explain why the conditions recorded in the info column are sufficient for their application. Since [7] is the same paper that uses the machine-generated differentials of this document to solve the Kervaire problem, the absence of a dependency analysis leaves open a circularity risk: if the proof of either theorem uses any differential that the program derives with it, the logical chain is circular. Please state the precise theorems, their hypotheses, and an explicit argument that they are independent of the machine results that the program proves using them.
[§4, Table of Proofs] The central artifact is a table of 21 million proof rows produced by the unverified program ./ss. There is no independent proof checker, no formal specification of the inference rules, and no soundness theorem for the program; a 'proof' row consists of assumption rows (reason='T') and deduction rows (reason='D') with natural-language justifications in the info column. The program's own assertion that a condition was 'checked' is the only evidence. To deserve the term 'machine proofs', the paper should provide an auditable mechanism: for example, a formal checker for the proof logs, an independent reimplementation, or a precise operational semantics of ./ss's inference steps together with a theorem that every generated row is valid in the Adams spectral sequence.
[§3, Notation 3.5] The data encoding assumes that all visible nontrivial differentials have length shorter than 1000. This assumption is stated but not justified or verified. If a differential of length at least 1000 occurs in the computed range, the level encoding would misclassify its target as a permanent cycle (level=9000), making the dataset interpretation unsound. Please provide a programmatic check that no such differential exists up to the stated internal degrees, or restrict the completeness claims of the dataset.
[§2.1, §2.3, §5] Several basis elements have d2=[NULL] (Section 2.1, Notation 2.3) and several displayed differentials are marked with '?' (for example, Table 25 rows 'x126,8,4+x126,8 d6 ?' and 'h6(C'+X2) d17 ?'; Table 24 row 'x126,18+e0x109,14,2 d7 ?'). The paper should clarify which entries are asserted to be fully resolved with machine proofs and which remain undetermined, and it should state explicitly whether the Kervaire-critical rows used in [7] belong to the resolved class. As it stands, the reader cannot determine whether an unresolved '?' row is part of the advertised chain.
[§2, Remark 2.6] The naming convention for several CW spectra explicitly allows multiple homotopy types when the stated cofiber sequences exist, and the paper says it does not assume which one is picked. However, the Adams E2-page and subsequent differentials generally depend on the actual homotopy type, not only on the existence of cofiber sequences. The paper should either prove that the computed E2 data and proof logs are independent of these choices, or specify the precise models for the spectra in the dataset. Without this, the dataset's rows may not be well defined for every named spectrum.

minor comments (8)

[Throughout] The text contains numerous typos and missing spaces (e.g., 'Table1provides', 'Thecolumnname', 'Theprogram', and the word 'and' appearing as 'A' in the sentence beginning '...and we can get...'). A careful proofreading pass is needed.
[§2.1, Notation 2.1] The convention that x_i denotes ring generators and v_i denotes module generators is not consistently reflected in the tables of Section 5, where many symbols (e.g., x123,9, h6(C'+X2), [B4], M, g) are used without a glossary. Please add a reference to the definitions in the dataset or include a notation appendix.
[§2.2, Notation 2.8] The rules for determining the unique suspension k and the unique inclusion or quotient for maps named X__Y are stated informally; please give the precise criterion used by the program to select among candidates.
[§3, Tables 15–16] The examples of level encodings (e.g., level=9998, 9000, 2, 10000) are not annotated; a step-by-step decoding of one row from each table would greatly improve readability.
[§4, row reasons] The descriptions of reasons 'ToCs', 'OutCsI', and 'CsCm' are terse and would be considerably easier to trust with one concrete worked example for each reason, parallel to the examples already given for 'T' and 'D'.
[Table 11] Only 22 of the 49 spectra listed in Table 1 appear in Table 11 for computed d2 differentials; please state whether d2 is trivial, unknown, or simply omitted for the remaining spectra, and explain how ./ss handles missing d2 values in the proof system.
[§5, Tables 18–28] The tables list differentials without cross-references to the corresponding proof row ids in the Table of Proofs; adding an id column would make the individual machine proofs directly auditable.
[References] Since the Generalized Leibniz Rule and the Generalized Mahowald Trick are load-bearing for the proofs, the citation [7] should include specific theorem numbers, and the paper should note whether [7] is a preprint or accepted for publication.

Circularity Check

1 steps flagged · score 4.0 of 10

Machine-generated proofs depend on two companion-paper theorems whose only cited support is the same-authors Kervaire paper that consumes these very differentials; this is load-bearing self-citation, though not an equation-level definitional circle.

self citation load bearing [Section 1; Section 4 (rows with reason 'Syn', 'SynCs', 'SynIn'); Section 5]
"This program partially employs the Generalized Leibniz Rule and the Generalized Mahowald Trick—two theorems established in the paper [7] addressing the Last Kervaire Invariant Problem. These theorems enable the program to derive new differentials and extensions from previously computed ones. ... Rows with reason=‘Syn’. This means that the differential is obtained by the Generalized Leibniz Rule from the former row. ... Rows with reason=‘SynCs’. This means that the row is an extension and is obtained by the Generalized Mahowald Trick."

The proof table is the central artifact: Syn/SynCs/SynIn rows are the mechanism by which the program derives 'new differentials and extensions from previously computed ones.' Their justification is a citation to [7], a companion paper by the same three authors whose advertised conclusion, resolution of the Last Kervaire Invariant Problem, is, per the abstract and Section 5, fed by the machine differentials from this dataset. The present document neither states the two theorems nor shows that their proofs in [7] are independent of the Section 5 differentials (stems 122-127 of S0 and stem 126 of S0/nu). If the generalized theorems in [7] rely on any of those differentials, the derivation forms a cycle.

full rationale

The paper's derivation chain is not a simple fit or renaming: the Adams E2 data come from the first author's program ./Adams implementing an external secondary-Steenrod-operation algorithm cited to Chua and Nassau, and three manually added differentials are sourced to the image of J and to Bruner–Rognes power operations, which are independent inputs. The main reason the score is not 0-2 is that the machine proof table, which is the central claim of the document, relies on the Generalized Leibniz Rule and the Generalized Mahowald Trick as inference rules, and those rules are cited only to the authors' own companion paper [7]. The companion paper is not an external or machine-checked certificate within this document, and it is the same paper whose Kervaire conclusion is built from the differentials that these rules help produce. That is a genuine self-citation dependency, and the paper provides no proof that the cited theorems are independent of the machine outputs. However, no specific equation-level reduction or fitted-parameter reproduction is exhibited: the proof table contains concrete case analyses, contradiction arguments, and naturality/Leibniz steps, and the d2 base data are computed by an independently described algorithm. The circularity is therefore partial and structural—a load-bearing reliance on same-author results whose independence is not demonstrated—rather than a case where a 'prediction' equals its input by construction.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claim rests on a large software computation and on theorems from the companion paper [7]. The axioms are the correctness of the programs, the validity of the Generalized Leibniz Rule and Generalized Mahowald Trick, the accuracy of three manually added differentials from prior literature, and the assumption that differentials have length shorter than 1000.

assumptions (5)

domain assumption The programs ./Adams and ./ss correctly implement the Adams E2 computation and the spectral sequence machinery.
All machine outputs depend on the correctness of these programs, which are by the first author and not independently verified.
domain assumption The Generalized Leibniz Rule and the Generalized Mahowald Trick, established in the companion paper [7], are valid and can be used as inference rules.
These theorems from [7] are used by the program ./ss to derive new differentials and extensions; the present paper does not prove them.
domain assumption Three manually added differentials are correct: d5 h2^4 h6 = h2^0 P^6 d0, d6 h5^5 h7 = h2^0 x126,60 in S0, and d3 v2^16 = beta5 g in tmf.
Taken from the image of J and from Bruner-Rognes [2]; not generated by the program.
ad hoc to paper All visible nontrivial differentials in the dataset have length shorter than 1000.
Stated in Notation 3.5; used to interpret the level values in the differential tables.
domain assumption The CW spectra with the given names exist and satisfy the stated cofiber sequences.
Remark 2.6 notes that names may represent any homotopy type satisfying the conditions, and the programs use only the cofiber sequences.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Machine Proofs for Adams Differentials and Extension Problems among CW Spectra." pith.science (2026). https://pith.science/paper/BJ5GUP4F

@misc{pith2026241210876,
  author       = {Pith},
  title        = {Pith review of: Machine Proofs for Adams Differentials and Extension Problems among CW Spectra},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BJ5GUP4F}},
  note         = {Machine review of arXiv:2412.10876}
}

read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

On the Last Kervaire Invariant Problem
math.AT 2024-12 conditional novelty 8.0 of 10

This paper proves that the element h_6^2 is a permanent cycle in the Adams spectral sequence, thereby establishing the existence of framed manifolds of Kervaire invariant one in dimension 126 and resolving the Kervair...

Reference graph

Works this paper leans on

9 extracted references · 7 canonical work pages · cited by 1 Pith paper

[7]

On the Last Kervaire Invariant Problem.arXiv Preprint, arXiv:2412.10879, 2024

Weinan Lin, Guozhen Wang, and Zhouli Xu. On the Last Kervaire Invariant Problem.arXiv Preprint, arXiv:2412.10879, 2024

arXiv 2024
[1]

M. G. Barratt, J. D. S. Jones, and M. E. Mahowald. The Kervaire invariant problem. InPro- ceedings of the Northwestern Homotopy Theory Conference (Evanston, Ill., 1982) , volume 19 of Contemp. Math., pages 9–22. Amer. Math. Soc., Providence, RI, 1983

work page 1982
[2]

Bruner and John Rognes

Robert R. Bruner and John Rognes. The Adams spectral sequence for topological modular forms, volume 253 ofMathematical Surveys and Monographs. American Mathematical Society, Providence, RI, [2021]©2021

work page 2021
[3]

TheE3 page of the Adams spectral sequence.arXiv preprint, arXiv.2105.07628, 2021

Dexter Chua. TheE3 page of the Adams spectral sequence.arXiv preprint, arXiv.2105.07628, 2021

arXiv 2021
[4]

Github repo.https://github.com/WayneLin92/SSeqCpp Github Webpage 2024

Weinan Lin. Github repo.https://github.com/WayneLin92/SSeqCpp Github Webpage 2024

work page 2024
[5]

Interactive plot of the Adams spectral sequence.https://waynelin92.github

Weinan Lin. Interactive plot of the Adams spectral sequence.https://waynelin92.github. io/ss/kervaire-49.html Github Webpage 2024

work page 2024
[6]

Machine proofs for Adams differentials and extension problems among CW spectra

Weinan Lin, Guozhen Wang, and Zhouli Xu. Machine proofs for Adams differentials and extension problems among CW spectra. Zenodo.https://doi.org/10.5281/zenodo.14272279 December 2024

work page doi:10.5281/zenodo.14272279 2024
[8]

On the secondary Steenrod algebra.New York J

Christian Nassau. On the secondary Steenrod algebra.New York J. Math. , 18:679–705, 2012

work page 2012

Show all 9 references

[9]

The strong Kervaire invariant problem in dimension 62.Geom

Zhouli Xu. The strong Kervaire invariant problem in dimension 62.Geom. Topol., 20(3):1611– 1624, 2016

2016

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [7]

On the Last Kervaire Invariant Problem.arXiv Preprint, arXiv:2412.10879, 2024

Weinan Lin, Guozhen Wang, and Zhouli Xu. On the Last Kervaire Invariant Problem.arXiv Preprint, arXiv:2412.10879, 2024

arXiv 2024

[2] [1]

M. G. Barratt, J. D. S. Jones, and M. E. Mahowald. The Kervaire invariant problem. InPro- ceedings of the Northwestern Homotopy Theory Conference (Evanston, Ill., 1982) , volume 19 of Contemp. Math., pages 9–22. Amer. Math. Soc., Providence, RI, 1983

work page 1982

[3] [2]

Bruner and John Rognes

Robert R. Bruner and John Rognes. The Adams spectral sequence for topological modular forms, volume 253 ofMathematical Surveys and Monographs. American Mathematical Society, Providence, RI, [2021]©2021

work page 2021

[4] [3]

TheE3 page of the Adams spectral sequence.arXiv preprint, arXiv.2105.07628, 2021

Dexter Chua. TheE3 page of the Adams spectral sequence.arXiv preprint, arXiv.2105.07628, 2021

arXiv 2021

[5] [4]

Github repo.https://github.com/WayneLin92/SSeqCpp Github Webpage 2024

Weinan Lin. Github repo.https://github.com/WayneLin92/SSeqCpp Github Webpage 2024

work page 2024

[6] [5]

Interactive plot of the Adams spectral sequence.https://waynelin92.github

Weinan Lin. Interactive plot of the Adams spectral sequence.https://waynelin92.github. io/ss/kervaire-49.html Github Webpage 2024

work page 2024

[7] [6]

Machine proofs for Adams differentials and extension problems among CW spectra

Weinan Lin, Guozhen Wang, and Zhouli Xu. Machine proofs for Adams differentials and extension problems among CW spectra. Zenodo.https://doi.org/10.5281/zenodo.14272279 December 2024

work page doi:10.5281/zenodo.14272279 2024

[8] [8]

On the secondary Steenrod algebra.New York J

Christian Nassau. On the secondary Steenrod algebra.New York J. Math. , 18:679–705, 2012

work page 2012