Prove Naimark (openai/math family 297: A ZFC counterexample to Naimark's problem) in Lean 4 with Mathlib…
Prove Naimark (openai/math family 297: A ZFC counterexample to Naimark's problem) in Lean 4 with Mathlib…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 297 of the release, A ZFC counterexample to Naimark's problem (Operator algebras). The…
The task
Context: this statement belongs to family 297 of the release, *A ZFC counterexample to Naimark's problem* (Operator algebras). The family as a whole: Gives an alternative to \href{https://arxiv.org/abs/2609.26930v1}{Tanaka's ZFC construction} of a unital infinite-dimensional simple complex $C^*$-algebra with a…
Part of raising-heart/openai-math.