we-solve (beta)

Math-2198-A1 · revision r1 · on Math-2198

OpenAI claim summary for Math-2198

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: 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.

Nine-dimensional diameter covering: The nine-dimensional bounded rank-one-projector example needs more than ten smaller-diameter sets, a direct counterexample to the universally quantified Borsuk assertion.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

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

Manuscript

Contents
  1. Borsuk's Conjecture
  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's Conjecture

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$. It supplies a counterexample in dimension nine rather than deciding every dimension from four onward.

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