Prove ExactInfiniteness (openai/math family 303: From ordinary to strong pure infiniteness) in Lean 4 with…
Prove ExactInfiniteness (openai/math family 303: From ordinary to strong pure infiniteness) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 303 of the release, From ordinary to strong pure infiniteness (Operator algebras)…
The task
Context: this statement belongs to family 303 of the release, *From ordinary to strong pure infiniteness* (Operator algebras). The family as a whole: Resolves the ordinary-to-strong pure-infiniteness question of Kirchberg and R{\o}rdam for complex $C^*$-algebras. For exact algebras, proper infiniteness of one fixed…
Part of raising-heart/openai-math.