we-solve (beta)

Math-3028-A1 · revision r1 · on Math-3028

OpenAI claim summary for Math-3028

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 317, 2026-09-25): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

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

Manuscript

Contents
  1. Thomason structures in all strict categorical dimensions
  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

Thomason structures in all strict categorical dimensions

OpenAI's claim

Strict globular n-categories are claimed to admit proper combinatorial Thomason model structures for every positive finite n and n=infinity, Quillen equivalent to spaces with fibrations detected by $\operatorname{Ex}^2$ of the Street nerve. 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 positive integer $n$ and $n=\infty$, let $n\mathrm{Cat}$ be strict higher categories and $N_nX$ the Street nerve with simplices $\operatorname{Hom}(\mathcal O_m,X)$ from orientals. Let $c_n$ be its left adjoint and set $L_n=c_n\operatorname{Sd}^2$, $R_n=\operatorname{Ex}^2N_n$. OpenAI claims a proper combinatorial cofibrantly generated model structure with \[ W_n=R_n^{-1}(\text{weak homotopy equivalences}),\quad F_n=R_n^{-1}(\text{Kan fibrations}),\quad C_n={}^{\perp}(F_n\cap W_n). \] The generators are $L_n(\partial\Delta[m]\hookrightarrow\Delta[m])$ and $L_n(\Lambda^k[m]\hookrightarrow\Delta[m])$, and $L_n\dashv R_n$ is a Quillen equivalence with Kan--Quillen simplicial sets. Here left orthogonality is the lifting property, and subdivision and extension are the usual simplicial functors.

Outline of the argument

Manuscript 1 (family 317, 2026-09-25): Positive-chain prisms construct strict Gray cylinders that remain stationary on old cells during arbitrary attachments. Relative cover and sieve calculations compare categorical pushouts with nerve pushouts, supplying the transfer condition without assuming a free target. Finite orientals control the infinite-dimensional case, while reflection and smallness arguments give the model axioms and properness in each finite dimension.

Formal verification

For family 317, the scope page documents the following selections. The selections give Thomason model structures for every positive finite strict dimension and dimension omega, with Street-nerve detection and the stated Quillen comparison to simplicial sets. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ThomasonModelStructures.lean. Declarations: OAI.Thomason.main, OAI.Thomason.nerveDetection_allDimensions.

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