∑math20

Theoretical computer science · Result 127

Average sensitivity of polynomial threshold functions

1 paperLean

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\), uniformly for \(1\le d\le n\). Average sensitivity counts expected output changes under single-bit flips. This establishes the asymptotic Gotsman–Linial conjecture, allowing polynomial zeros with \(\mathop{\mathrm{sign}}\nolimits (0)=1\).

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Average sensitivity of polynomial threshold functions

Average sensitivity of polynomial threshold functions

OpenAI · September 25, 2026

For every n ≥ 1 and \(1\le d\le n\), we prove that a polynomial threshold function of degree at most d on the uniform Boolean cube has average sensitivity at most \(8d\sqrt n\). This proves the asymptotic form of the Gotsman–Linial conjecture. The bound is uniform in both parameters and uses the convention \(\mathop{\mathrm{sgn}}\nolimits (0)=1\).

Read PDF Download Source

Cite
@misc{OAI:Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026,
  author = {{OpenAI}},
  title = {{Average sensitivity of polynomial threshold functions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/main.pdf}{OAI:Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalized result proves the average-sensitivity bound \(8d\sqrt n\) for every Boolean threshold function defined by a real multilinear polynomial of degree at most \(d\) on the \(n\)-dimensional cube. The sign convention assigns value \(1\) at zero. This establishes the stated asymptotic bound, rather than the separate conjecture identifying exact extremizers.

Comparator links

ResultComparator statement
Average sensitivity of polynomial threshold functionsGotsmanLinial.lean

Scope note on GitHub →