Prove DepthFive (openai/math family 135: Sharp homogeneous depth-five complexity of matrix products) in Lean…
Prove DepthFive (openai/math family 135: Sharp homogeneous depth-five complexity of matrix products) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 135 of the release, Sharp homogeneous depth-five complexity of matrix products…
The task
Context: this statement belongs to family 135 of the release, *Sharp homogeneous depth-five complexity of matrix products* (Theoretical computer science). The family as a whole: Over every characteristic-zero field, the $(1,1)$ entry of a product of $n$ independent $n\times n$ variable matrices requires…
Part of raising-heart/openai-math.