Prove ProductBrown (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean…
Prove ProductBrown (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 293 of the release, A counterexample to the hyperinvariant-subspace problem…
The task
Context: this statement belongs to family 293 of the release, *A counterexample to the hyperinvariant-subspace problem* (Operator algebras). The family as a whole: Constructs a nonzero norm-quasinilpotent operator on every infinite-dimensional separable complex Hilbert space with no nonzero proper closed subspace…
Part of raising-heart/openai-math.