we-solve (beta)

Math-2198 · mathematics · Geometry

Borsuk's Conjecture

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
For every $n\geq1$, can each bounded subset of $\mathbb R^n$ with positive diameter be partitioned into at most $n+1$ subsets whose diameters are all strictly smaller than that of the original set?

Formulation references: [S1], [S2].

Short English statement

For every $n\geq1$, can each bounded subset of $\mathbb R^n$ with positive diameter be partitioned into at most $n+1$ subsets whose diameters are all strictly smaller than that of the original set?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2198-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2198

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.

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

Go to contribution →