AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A nine-dimensional counterexample to Borsuk's covering assertion

Does the classical conjecture or property hold, or does there exist a counterexample as established in A nine-dimensional counterexample to Borsuk's covering assertion?

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 156)

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A nine-dimensional counterexample to Borsuk's covering assertion'. The compact set of rank-one orthogonal projectors on ℝ4, with the Frobenius metric, cannot be covered by ten sets of strictly smaller diameter. It therefore gives a counterexample to Borsuk's conjecture in dimension nine.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 156). The Lean development was not rebuilt locally.