The modified integer round-up conjecture for bin packing
From OpenAI Aftermath
The modified integer round-up conjecture for bin packing, posed by Scheithauer and Terno in the 1990s, asserts that the minimum number of bins never exceeds the value of the Gilmore–Gomory configuration linear program, rounded up, by more than one. A related algorithmic question, listed by Williamson and Shmoys among the open problems of their 2011 textbook, asks whether a polynomial-time algorithm can always come within a fixed additive constant of the optimum. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that the configuration gap is unbounded and that every fixed additive approximation is NP-hard, with a Lean formalization. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The configuration linear program assigns nonnegative weights to feasible bin patterns and covers the item demands; its cutting-stock antecedents include Eisemann's formulation and Gilmore and Gomory's column-generation method. Its value is a lower bound on the optimum. Marcotte exhibited an instance for which the integer round-up property, optimum equal to the rounded-up linear-programming value, fails, and Scheithauer and Terno investigated the modified bound with an allowance of one bin.
- Fernandez de la Vega and Lueker obtained an asymptotic approximation scheme, Karmarkar and Karp an additive error of order log2 OPT, and Rothvoss and then Hoberg and Rothvoss smaller logarithmic additive errors. Whether one algorithm can guarantee OPT + C bins for an absolute constant C remained open.
The original result
- Claims. The first theorem of Additive hardness and unbounded configuration gaps in bin packing states that for every integer c ≥ 0 there are a finite rational bin-packing instance with every item size above 1/6 and an integer B such that the configuration linear program has value exactly B while the optimum exceeds B + c; the same value holds for the configuration program whose patterns are subsets of the individual item copies. Taking c = 1 disproves the modified integer round-up conjecture without any complexity assumption. The second theorem states that for every fixed c it is NP-hard to distinguish instances that pack into B bins from instances that do not pack into B + c bins, again with all item sizes above 1/6, so that at most five items fit in a bin; a corollary states that a deterministic polynomial-time algorithm with an absolute additive guarantee exists if and only if P = NP.
- Method, as described: a reduction from vertex cover in which each vertex is represented by two competing rooted trees with shared quotas, encoded as interval cells and five-item bins whose sizes enforce the intended patterns; an exact fractional packing gives the configuration value, and any packing with few extra bins is converted into a small vertex cover.
- Source (openai/math repository, commit
7ef5c0c): Additive hardness and unbounded configuration gaps in bin packing, dated 24 September 2026. - Formalization, as described by the repository. The scope note lean/docs/118.md states that the formalized results rule out a universal additive bound for the configuration linear program, give NP-hardness of distinguishing B from B + c bins for each fixed c, and show that a deterministic polynomial-time algorithm with a fixed absolute additive allowance exists exactly when P = NP. The Comparator statement is
BinPackingGap.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 29 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Bin packing: additive error and configuration gaps, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains bin patterns and fractional packings, the structural gap and the algorithmic hardness, a reduction that controls arbitrary packings, prefix counts that turn bins into interval coverage, edge permits and conservation, an exact fractional witness, and the passage from satisfiability gaps to additive hardness, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-07 | E. Winnington, Unbounded Integrality Gaps and Additive Hardness for the Skiving Stock Problem, a manuscript in the GitHub repository ewinnington/math | Extension (transfer to bin covering) | Transfers the bin-packing construction to the skiving stock problem, also called bin covering, by complementing item sizes. It claims that the additive gaps of both the ordinary and the proper pattern linear programs are unbounded, which refutes Zak's modified integer round-down property, and that every fixed additive allowance is NP-hard. It uses the two results of the manuscript as inputs and proves the transfer itself. | Manuscript in a public repository, commit of 7 October 2026. It states that the proof was generated by a combination of Anthropic Fable 5.1 and OpenAI GPT 5.6 Sol Pro. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a Comparator pass for BinPackingGap on 10 October 2026, with the standard axioms. It notes that P and NP are defined through Mathlib's polynomial-time Turing machines and a certificate definition. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | Configuration gaps in bin packing, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Six lessons: bin packing and the configuration program, two competing trees, coordinates, cells and items, sizes that enforce the patterns, packings from covers and a fractional packing, and extracting a vertex cover. | The course states that it was written and self-checked by Claude Opus 5.5 (Anthropic) and that independent review is not complete. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38074613260 | Verification (kernels) | Records that Lean's default kernel accepts the BinPackingGap solution and that the nanoda kernel did not, after 1,426 s; an earlier run was terminated by the runner. The project's draft comment to the nanoda maintainers lists this challenge among exports that overflow nanoda's fixed 16 MiB worker stack, a resource limit rather than a logical rejection. The project reports two-kernel certification of 398 of 416 challenges, and this challenge is not among them. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list BinPackingGap, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | AI Proved What?, episode 118 One more bin?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of both theorems and of the vertex-cover reduction. The episode states that the instances grow very rapidly with c, so the result is compatible with the logarithmic additive algorithms, that no matching logarithmic lower bound in terms of the instance size is obtained, and that the hardness concerns deterministic algorithms with a fixed additive allowance. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 26 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: OpenAI published a Lean proof of both theorems and the equivalence with P = NP, not run by the site. The page states that the formalization has 284 files and 158,527 lines, that it found no unproved steps by search, and that it has seen no expert review. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
