Hovey-Strickland finite-generation question: are the homotopy groups of the $K(n)$ -local sphere finitely generated over $\mathbb Z_p$ ?

Fix a prime $p$ and height $n\ge1$ , and let $L_{K(n)}S$ be the Bousfield localization of the $p$ -complete sphere at Morava $K$ -theory $K(n)$ . It is not connective, so finiteness must be controlled degree by degree. At height one the answer follows from the classical computation; at height two and $p\ge5$ Hovey and Strickland derived it from Shimomura's computations. Is $\pi_t L_{K(n)}S_p^\wedge$ a finitely generated $\mathbb Z_p$ -module for every prime $p$ , every height $n$ and every integer $t$ ?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Stable homotopy theory; chromatic homotopy
Posed by: Mark Hovey and Neil Strickland, Problem 16.2 of 'Morava K-theories and localisation' (Memoirs AMS, 1999); also Problem 1 of Hovey's Morava K- and E-theory problem list
Year posed: 1999
Years open: 27y
Solved: 2026-09-24
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Unreviewed
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 26 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: for every prime $p$ , height $n\ge1$ and integer $t$ , $\pi_t L_{K(n)}S_p^\wedge$ is a finitely generated $\mathbb Z_p$ -module; equivalently $\pi_t L_{K(n)}F$ is finitely generated for every finite $p$ -local spectrum $F$ . Combined with the rational computation of Barthel-Schlank-Stapleton-Weinstein this fixes the free ranks. The key step is finiteness of continuous cohomology of the stabilizer with mod $p$ Lubin-Tate coefficients. It gives no bound on the number of generators or the torsion as $p$ , $n$ , $t$ vary, computes no torsion, and does not extend to all invertible $K(n)$ -local spectra (known to fail at height two).

What the AI did

The release README says the results were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human-edited). The manuscript is authored 'OpenAI' and names no human author.

Verification

No independent mathematician has checked this yet. Checked here: the introduction, history section and Theorem 1.1 were read against Hovey-Strickland Problem 16.2. lean/docs/313.md does not exist at the pinned commit and formalization.yaml has no entry for this manuscript, so there is no formal statement. The proof leans on deep external inputs (Fargues-Fontaine curve geometry, Fargues-Scholze, Anschutz-Le Bras relative full faithfulness, Devinatz-Hopkins descent, Mathew's descendability) that a reader has to accept.

Source

CodeOpenAI math release: Finite generation for the K(n)-local sphere

Hovey-Strickland finite-generation question: are the homotopy groups of the K(n)K(n)K(n)-local sphere finitely generated over Zp\mathbb Z_pZp​?

What was actually shown

What the AI did

Verification

Source

Discussion

Hovey-Strickland finite-generation question: are the homotopy groups of the $K(n)$ -local sphere finitely generated over $\mathbb Z_p$ ?