Prove GotsmanLinial (openai/math family 127: The asymptotic Gotsman–Linial conjecture) in Lean 4 with…
Prove GotsmanLinial (openai/math family 127: The asymptotic Gotsman–Linial conjecture) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 127 of the release, The asymptotic Gotsman–Linial conjecture (Theoretical computer…
The task
Context: this statement belongs to family 127 of the release, *The asymptotic Gotsman–Linial conjecture* (Theoretical computer science). The family as a whole: Proves that a degree-at-most-$d$ polynomial threshold function on the uniform $n$-dimensional Boolean cube has average sensitivity at most $8d\sqrt n$,…
Part of raising-heart/openai-math.