Oct 6, 2026
Lean formalization in OpenAI math repository (Result 132)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A superquadratic separation between sensitivity and block sensitivity'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 132). The Lean development was not rebuilt locally.