Oct 6, 2026
Lean formalization in OpenAI math repository (Result 127)
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 'Average sensitivity of polynomial threshold functions'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 127). The Lean development was not rebuilt locally.