Boolean functions violate the square-root degree bound by arbitrary factors

1 paperLean

Disproves the proposed square-root bound relating a Boolean function's linear Fourier coefficients to its polynomial degree. For every C > 0, there is a sign-valued Boolean function f with \(\sum_i\widehat f(\{i\})\gt C\sqrt{\deg(f)}\). Thus its total signed correlation with individual input bits can exceed the proposed bound by an arbitrary factor.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Unbounded Violations of the Square-Root Degree Bound

OpenAI · September 26, 2026

We disprove the Gopalan–Servedio square-root conjecture, even up to an arbitrary constant factor. For every real C > 0, there is a nonconstant Boolean function \(f:\{-1,1\}^n\to\{-1,1\}\) on a finite sign cube such that \(\displaystyle \sum_{i=1}^n \widehat f(\{i\})\gt C\sqrt{\deg(f)}.\) Here \(\widehat f(\{i\})\) is the linear Fourier coefficient associated with the ith input, and \(\deg(f)\) is the degree of the real multilinear polynomial representing f.

Read PDF Download Source

Cite

@misc{OAI:Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026,
  author = {{OpenAI}},
  title = {{Unbounded Violations of the Square-Root Degree Bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026.pdf}{OAI:Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Unbounded Violations of the Square-Root Degree Bound

Scope

The formalization disproves the Gopalan–Servedio square-root degree conjecture by an unbounded factor. For every \(C>0\), it gives a nonconstant Boolean function on a finite sign cube for which the sum of its linear Fourier coefficients exceeds \(C\sqrt{\deg f}\), where \(\deg f\) is its real multilinear degree.

It also proves that the ratio of the sum of the absolute values of those coefficients to \(\sqrt{\deg f}\) is unbounded among positive-degree Boolean functions.

Comparator links

Result	Comparator statement
Unbounded violations of the square-root Fourier-degree bound	SquareRootDegree.lean

Scope note on GitHub →