Prove DoublingHilbert (openai/math family 098: A negative answer to the Lang–Plaut problem) in Lean 4 with…
Prove DoublingHilbert (openai/math family 098: A negative answer to the Lang–Plaut problem) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 098 of the release, A negative answer to the Lang–Plaut problem (Convex and metric…
The task
Context: this statement belongs to family 098 of the release, *A negative answer to the Lang–Plaut problem* (Convex and metric geometry). The family as a whole: Every infinite-dimensional real Banach space contains a compact doubling set that admits no bi-Lipschitz embedding into any finite-dimensional normed space.…
Part of raising-heart/openai-math.