we-solve (beta)

Math-2606-A1 · revision r1 · on Math-2606

OpenAI claim summary for Math-2606

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Unbounded square-root-degree violations: The ratio of the absolute linear Fourier-coefficient sum to sqrt(exact multilinear degree) is unbounded among nonconstant Boolean functions.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Gopalan–Servedio square-root-degree Fourier bound
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Gopalan–Servedio square-root-degree Fourier bound

OpenAI's claim

Unbounded square-root-degree violations: The paper claims Boolean functions for which the sum of linear Fourier coefficients exceeds any prescribed multiple of the square root of the exact polynomial degree. The sum of their absolute values is consequently unbounded relative to that same scale.

Mathematical statement of the claimed result

Mathematical claim 1.
For uniform measure on $\{-1,1\}^n$, let $\widehat f(S)=\mathbb E[f(x)\prod_{i\in S}x_i]$ and $\deg f=\max\{|S|:\widehat f(S)\ne0\}$. The claim asserts \[\forall C>0\ \exists n\ge1\ \exists f:\{-1,1\}^n\to\{-1,1\}:\quad\deg f>0,\quad\sum_i\widehat f(\{i\})>C\sqrt{\deg f}.\] In particular $\sum_i|\widehat f(\{i\})|/\sqrt{\deg f}$ has no universal finite bound.

Outline of the argument

Unbounded square-root-degree violations: Finite observations are designed to retain variance more efficiently than they consume degree. Gaussian interval choices guide the report rules, and central-limit approximation realizes each stage with sufficiently large finite averages. Iterating the amplification criterion finitely many times yields any target ratio, after which a Boolean sign readout preserves the violation.

Formal verification

Family 192 describes Lean coverage for unbounded signed and absolute linear-Fourier-sum ratios relative to square-root degree.

Unbounded square-root-degree violations: The manuscript links SquareRootDegree.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources