∑math20

Theoretical computer science · Result 132

A superquadratic separation of sensitivity and block sensitivity

1 paperLean

Constructs total Boolean functions with block sensitivity \(\mathop{\mathrm{bs}}\nolimits (f)\ge s(f)^\alpha\) for a fixed α > 2, disproving the quadratic strengthening of the Sensitivity Conjecture. Here \(s(f)\) counts influential individual-bit flips, while block sensitivity allows disjoint groups of bits to change together.

Watch

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

Papers 1

First page of A superquadratic separation between sensitivity and block sensitivity

A superquadratic separation between sensitivity and block sensitivity

OpenAI · September 25, 2026

We disprove the quadratic strengthening of the Sensitivity Conjecture by constructing nonconstant total Boolean functions whose block sensitivity grows faster than any constant multiple of sensitivity squared. In fact, for some fixed α > 2, our examples have unbounded block sensitivity and satisfy \(\mathop{\mathrm{bs}}\nolimits (f)\ge s(f)^\alpha\).

Read PDF Download Source

Cite
@misc{OAI:A-superquadratic-separation-between-sensitivity-and-block-sensitivity-September-25-2026,
  author = {{OpenAI}},
  title = {{A superquadratic separation between sensitivity and block sensitivity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-superquadratic-separation-between-sensitivity-and-block-sensitivity-September-25-2026/paper.pdf}{OAI:A-superquadratic-separation-between-sensitivity-and-block-sensitivity-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 disproves a universal quadratic bound of block sensitivity by sensitivity for total Boolean functions. For every integer \(d\ge1\), it constructs a nonconstant function with \(\mathrm{bs}(f)/s(f)^2\ge2^d/(4(d+2)^2)\), making the ratio unbounded. The formalization also gives a fixed exponent \(\alpha>2\) and a sequence with \(s(f)^\alpha\le\mathrm{bs}(f,0)\) while the latter tends to infinity; here \(\mathrm{bs}(f,0)\) is block sensitivity at the all-zero input.

Comparator links

ResultComparator statement
Superquadratic sensitivity separationSensitivitySeparation.lean

Scope note on GitHub →