Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

The Hovey–Strickland and Chai conjectures

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves Chai’s invariant-ideal conjecture for Lubin–Tate deformation rings over finite residue fields, at every prime and positive height n. Through the implication of Barthel–Heard–Naumann, this proves the Hovey–Strickland conjecture: dualizable \(K(n)\)-local spectra have exactly \(n+2\) thick tensor ideals, and their Balmer spectrum is a chain of \(n+1\) points.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1 (Stabilizer-invariant ideals)

In Stabilizer orbits and thick tensor ideals of dualizable K(n)-local spectra, 24 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

Let U\subseteq A_n^\times be any open subgroup. The proper prime ideals of E_0 stabilized by U are precisely

0,\ I_1,\ldots,I_n.

The U-invariant radical ideals are precisely

0,\ I_1,\ldots,I_n,\ E_0.

The latter list also gives the radical ideals invariant under the full canonical G_n-action.

Theorem 1.2 (Hovey–Strickland conjecture)

In Stabilizer orbits and thick tensor ideals of dualizable K(n)-local spectra, 24 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

For every prime p and every n\geq 1, the thick tensor ideals of \mathcal D_{(n,p)} are exactly

\mathcal D_{(n,p)}=\mathcal D_0 \supsetneq\mathcal D_1\supsetneq\cdots \supsetneq\mathcal D_n\supsetneq\mathcal D_{n+1}=0.

In particular, there are n+2 such ideals, and each \mathcal D_k is independent of the chosen finite type-k spectrum.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

Reported proof verification
The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations
One current paper, readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Stabilizer orbits and thick tensor ideals of dualizable K(n)-local spectra

24 September 2026, current edition.

Read it herePDF

We classify the prime and radical ideals of the Lubin–Tate deformation ring invariant under an open Morava stabilizer subgroup, at every prime and positive height. This proves Chai’s invariant-ideal conjecture in the standard finite-residue-field formulation. It also proves the Hovey–Strickland conjecture: the dualizable \(K(n)\)-local category has exactly \(n+2\) thick tensor ideals, and its Balmer spectrum is a chain of \(n+1\) points.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

  • From github.com/mahrud/openai-math-comments, 9 October 2026. Source

    Points to arXiv:2610.10072, whose author reports OpenAI’s family 311 paper uses the same strategy and notation as their earlier draft and notes a separate proof by Ningyi Li.

  • Chenglong Ma, Invariant Primes in Lubin-Tate Space and Hovey-Strickland at Every Height, 7 October 2026. Source

    Chenglong Ma writes that OpenAI’s Hovey-Strickland manuscript matches the strategy and notation of a draft of their paper that they uploaded to ChatGPT on 8 September 2026, and that Ningyi Li had also proved the result independently.

  • Chenglong Ma, Invariant Primes in Lubin-Tate Space and Hovey-Strickland at Every Height, 7 October 2026. Source

    Author states the OpenAI Hovey-Strickland paper matches a preliminary version they uploaded to ChatGPT on 8 Sep 2026.

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

  • Family 311 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

  • Family 311 The release has no Lean statement for this family. Open the form