we-solve (beta)

Math-3022-A1 · revision r1 · on Math-3022

OpenAI claim summary for Math-3022

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Manuscript 1 (family 319, 2026-09-26): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed counterexample to that assertion in full.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Hahn–Wilson thick generation at fp-type two
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Hahn–Wilson thick generation at fp-type two

OpenAI's claim

For sufficiently large primes, a connective p-complete spectrum of exact fp-type two is claimed not finitely constructible from standard BP<2>, despite satisfying both finite-localization and telescope-to-Morava comparison equivalences. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
For every sufficiently large prime $p$, OpenAI claims a connective completed spectrum $X$ with finitely presented mod-$p$ cohomology over the Steenrod algebra, of exact fp-type two, satisfying \[ X\notin\operatorname{Thick}(BP\langle2\rangle_p^\wedge),\qquad L_2^fX\simeq L_2X,\qquad L_{T(2)}X\simeq L_{K(2)}X. \] Fp-type at most $n$ means $\pi_*(V\wedge X)$ has finitely many nonzero finite groups for some, equivalently every, finite type-$(n+1)$ spectrum $V$; exact type two excludes type at most one. Thick closure permits finite sums, shifts, cofibers and retracts, not arbitrary colimits. Here $L_2=L_{E(2)}$, $L_2^f$ is finite localization away from type greater than two, and $T(2)$ a height-two periodic telescope. The Brown--Peterson generator uses the specified standard form with coefficients $\mathbb Z_p[v_1,v_2]$.

Outline of the argument

Manuscript 1 (family 319, 2026-09-26): Large-prime algebraicity transfers the problem to periodic sheaf complexes, where Laurent operators create paired defects growing faster than the available kernel bounds. The resulting homology-to-dual-homology restriction removes each possible finite tower stage by backward induction, including retracts. Completion remains locally controlled, allowing a connective cover with the required fp-type and localization equivalences while preserving the global obstruction.

Formal verification

Family 319 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources