Finite generation of the homotopy of the K(n)-local sphere
From OpenAI Aftermath
Finite generation of the homotopy of the K(n)-local sphere is the question, posed by Hovey and Strickland, whether every homotopy group of the K(n)-localized sphere is a finitely generated module over the p-adic integers, at every prime p, positive height n and integer degree. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a positive answer. The collection includes no Lean formalization of this result. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The question is Problem 16.2 of Hovey and Strickland and Problem 1 of Hovey's list of problems on Morava K- and E-theory; in Li's terminology it asks whether the local sphere is of finite type.
- At height one the local sphere is the fiber of an Adams operation on completed K-theory. At height two and p ≥ 5, Hovey and Strickland's analysis of Shimomura's calculations gives finiteness of every homotopy group of LK(2)F for finite torsion spectra F. Devinatz studied finiteness properties of homotopy fixed points for smaller subgroups of the Morava stabilizer.
- Barthel, Schlank, Stapleton and Weinstein determined the rational homotopy of the K(n)-local sphere at every prime and height; the manuscript notes that this does not bound the integral torsion.
The original result
- Claim. Theorem 1.1 of Finite generation for the K(n)-local sphere states that for every prime p, every integer n ≥ 1 and every integer t, the Zp-module πtLK(n)Sp is finitely generated; equivalently, the same holds for K(n)-localizations of finite p-local spectra. The manuscript states that no uniform bound on the number of generators or on the torsion is asserted, and that together with the rational computation of Barthel–Schlank–Stapleton–Weinstein the theorem determines the free ranks.
- Method, as described: the central input is the finiteness of the continuous cohomology of the stabilizer group with coefficients in Morava E-theory modulo p, proved for a larger class of coefficient modules by downward induction over the height strata of the deformation space: finite boundary strips have finite cohomology by induction, and open-stratum cohomology is shown to be countable using finite covers that mark the formal group and its Tate module, so that compact countable cohomology is finite. Morava descent for the Moore spectrum with a horizontal vanishing line and compact Nakayama then give the integral statement.
- Sources. The manuscript Finite generation for the K(n)-local sphere at commit
1581d4c. - Formalization. The repository has no Lean scope note for this family.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-09 | justinli1128/OnOpenAiPreprint313-finiteGenerationOfK-n-LocalSphere (GitHub) | Reading (exposition) | A repository for a website presenting the manuscript and the Hovey–Strickland question it answers. | The README consists of this one-line description. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes in what it audited: the introduction, the descent spectral sequence with its horizontal vanishing line and the compact Nakayama step, the height induction with the finite marking descent, and Sections 9 and 10, read line by line. It states that the geometric Sections 4–8, among them the completed-tower identification on the relative Fargues–Fontaine curve, the Kummer support calculations and the Cartier transfer, were not verified in detail, that the whole result rests on them, and that its verdict is therefore not a confirmation of the theorem. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- A different question about the same category, the classification of its thick tensor ideals, is treated on the page The Hovey–Strickland conjecture.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
