OpenAI claim summary for Math-2820

Individual and strong pure infiniteness

OpenAI's claim

Proper infiniteness of all positive elements is claimed to imply strong pure infiniteness; under exactness a uniform finite-amplification version suffices, and separable nuclear algebras with that property absorb O_infinity. 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 an exact complex $C^*$-algebra $C$, assume one fixed $n\ge1$ makes every amplified positive element $h^{\oplus n}$ properly infinite, meaning $h^{\oplus n}\oplus h^{\oplus n}\precsim h^{\oplus n}$ in Cuntz comparison. OpenAI claims every positive $h\in C$ is itself properly infinite and $C$ is strongly purely infinite. Its other theorem omits exactness but assumes every positive element already properly infinite. For all $a,b\ge0$, arbitrary $c\in C$ and $\varepsilon>0$, it claims $s,t\in C$ with \[ \|s^*as-a\|<\varepsilon,\qquad\|t^*bt-b\|<\varepsilon,\qquad\|s^*ct\|<\varepsilon. \] These are simultaneous diagonalization inequalities, not only individual positive-element comparison.

Outline of the argument

Manuscript 1 (family 303, 2026-09-25): Graph shrinking and polar deformation merge hereditary positive elements while retaining norm signals in all required quotients. Exactness rules out persistent amplification obstructions, while a separate nuclear argument uses matrix norms forbidden in exact targets. Controlled comparison coefficients then eliminate arbitrary mixed entries, establishing strong diagonalization and the central-sequence absorption conclusion.

Formal verification

For family 303, the scope page documents the following selections. One selection derives strong pure infiniteness directly from proper infiniteness of each positive element. The fixed-amplification variant assumes exactness; no general absorption conclusion is selected without its additional hypotheses. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ExactInfiniteness.lean, IndividualStrongInfiniteness.lean. Declarations: OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_individuallyProperlyInfinite_any, OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite, OAI.MainGap.Manuscript.individual_to_strong_main.

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

• OpenAI, Weak pure infiniteness and O _$\infty$ absorption, 2026-09-25; citation key OAI:Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:exact-infiniteness; Statement source: thm:individual-to-strong.
• Family 303: Lean scope.
• Comparator ExactInfiniteness.json.
• Comparator ExactInfiniteness.lean.
• Comparator IndividualStrongInfiniteness.json.
• Comparator IndividualStrongInfiniteness.lean.
• OpenAI catalogue entry.