Prove MatrixFields (openai/math family 107: Matrix multiplication with exponent at most $9/4$) in Lean 4…
Prove MatrixFields (openai/math family 107: Matrix multiplication with exponent at most $9/4$) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 107 of the release, Matrix multiplication with exponent at most $9/4$ (Theoretical…
The task
Context: this statement belongs to family 107 of the release, *Matrix multiplication with exponent at most $9/4$* (Theoretical computer science). The family as a whole: Proves $\omega\le9/4$ over $\mathbb C$, giving $O_\varepsilon(n^{9/4+\varepsilon})$ arithmetic operations for square matrix multiplication. In…
Part of raising-heart/openai-math.