Oct 6, 2026
Lean formalization in OpenAI math repository (Result 112)
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 'Beyond the Square-Root Exponent for Depth-Three Boolean Circuits'. We construct a language in deterministic polynomial time whose n-bit membership function requires 2^{\omega(\sqrt n)} gates in an unbounded-fan-in OR–AND–OR circuit. The bound holds at every sufficiently large input length and counts all gates, including the bottom layer.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 112). The Lean development was not rebuilt locally.