Lean formalization in OpenAI math repository (Result 118)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Additive hardness and unbounded configuration gaps in bin packing'. We disprove the Modified Integer Round-Up Conjecture for bin packing by constructing instances with arbitrarily large additive gaps between the configuration-LP value and the integral optimum. We also prove that, for every fixed nonnegative integer c, distinguishing instances that fit in B bins from those requiring more than B+c bins is NP-hard. Both results hold with rational item sizes greater than 1/6, so each bin contains at most five items.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 118). The Lean development was not rebuilt locally.