Prove SmoothInitialForm (openai/math family 108: A cubic permanent–determinant lower bound) in Lean 4 with…
Prove SmoothInitialForm (openai/math family 108: A cubic permanent–determinant lower bound) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 108 of the release, A cubic permanent–determinant lower bound (Theoretical computer…
The task
Context: this statement belongs to family 108 of the release, *A cubic permanent–determinant lower bound* (Theoretical computer science). The family as a whole: Proves an $\Omega(n^3)$ lower bound for the border determinantal complexity of the $n\times n$ permanent over $\mathbb C$. Even coefficientwise limits of…
Part of raising-heart/openai-math.