we-solve (beta)

Math-2490-A1 · revision r1 · on Math-2490

OpenAI claim summary for Math-2490

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 at unsolvedmath.com: partially solved. 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.

For every $9\le d\le63$, the higher-dimensional corollary claims a compact diameter-$\sqrt2$ set needing more than $d+1$ smaller-diameter parts. It starts from the dimension-nine example and adjoins new equidistant points to raise the required number of parts. The cases $4\le d\le8$ are not decided by these constructions.

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

Manuscript

Contents
  1. Borsuk Partition Problem in Dimensions Four Through Sixty-Three
  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

Borsuk Partition Problem in Dimensions Four Through Sixty-Three

OpenAI's claim

Nine-dimensional diameter covering: The projector configuration of lines in $\mathbb R^4$, viewed in the nine-dimensional space of trace-one symmetric matrices, is claimed to require more than ten smaller-diameter covering sets. This compact configuration refutes Borsuk’s assertion in dimension nine.

Mathematical statement of the claimed result

Mathematical claim 1.
In the nine-dimensional affine space $\{A\in\operatorname{Sym}_4(\mathbb R):\operatorname{tr}A=1\}$ with Frobenius distance, set $X=\{uu^{\mathsf T}:u\in\mathbb R^4,\ |u|=1\}$. The claim is that $X$ is compact, $\operatorname{diam}X=\sqrt2$, and there do not exist ten subsets $X_1,\ldots,X_{10}$ covering $X$ with every $\operatorname{diam}X_i<\sqrt2$. The article also claims that, for each integer $d\ge9$, there is a compact $Y_d\subset\mathbb R^d$ of diameter $\sqrt2$ admitting no cover by $d+1$ subsets of smaller diameter. The extension adjoins $d-9$ points at diameter distance from one another and from the translated projector set. The dimensions four through eight remain outside these counterexamples.

Outline of the argument

Nine-dimensional diameter covering: A smaller-diameter cover is enlarged to an open cover and converted into nonnegative coordinate functions on projective three-space. Orthogonal lines must have disjoint positive supports. Extending the map to positive semidefinite matrices produces an odd sphere map; its mod-two degree and an equality analysis of the support complex contradict the possible ten-label structure.

Formal verification

Family 156 describes Lean coverage for the nine-dimensional projector covering obstruction against ten arbitrary smaller-diameter sets.

Nine-dimensional diameter covering: The manuscript links BorsukNine.lean (declaration OAI.BorsukNine.main_theorem).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources