ComparatorChallenges/BinPackingGap.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

75 declarations, 1 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Complexity.encodeWord line 9

    Also declared: OAI/Computability/BinPacking/Model.lean:9 (same declaration text).

  2. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 17

    Also declared: OAI/Computability/BinPacking/Model.lean:17 (same declaration text).

  3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.pairBits line 23

    Also declared: OAI/Computability/BinPacking/Model.lean:23 (same declaration text).

  4. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier line 26

    Also declared: OAI/Computability/BinPacking/Model.lean:26 (same declaration text).

  5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.Accepts line 32

    Also declared: OAI/Computability/BinPacking/Model.lean:32 (same declaration text).

  6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InNP line 37

    Also declared: OAI/Computability/BinPacking/Model.lean:37 (same declaration text).

  7. def OAI.BinPackingCompleteness.BinaryEncoding.bitsValue line 44

    Also declared: OAI/Computability/BinPacking/Model.lean:44 (same declaration text).

  8. def OAI.BinPackingCompleteness.BinaryEncoding.frame line 48

    Also declared: OAI/Computability/BinPacking/Model.lean:48 (same declaration text).

  9. def OAI.BinPackingCompleteness.BinaryEncoding.parseFrame line 52

    Also declared: OAI/Computability/BinPacking/Model.lean:52 (same declaration text).

  10. def OAI.BinPackingCompleteness.BinaryEncoding.nameBits line 59

    Also declared: OAI/Computability/BinPacking/Model.lean:59 (same declaration text).

  11. def OAI.BinPackingCompleteness.BinaryEncoding.parseName line 61

    Also declared: OAI/Computability/BinPacking/Model.lean:61 (same declaration text).

  12. structure OAI.BinPackingGap.Instance line 72

    Also declared: OAI/Computability/BinPacking/Model.lean:72 (same declaration text).

  13. abbrev OAI.BinPackingGap.Instance.Item line 80

    Also declared: OAI/Computability/BinPacking/Model.lean:80 (same declaration text).

  14. structure OAI.BinPackingGap.Packing line 84

    Also declared: OAI/Computability/BinPacking/Model.lean:84 (same declaration text).

  15. def OAI.BinPackingGap.HasPacking line 88

    Also declared: OAI/Computability/BinPacking/Model.lean:88 (same declaration text).

  16. def OAI.BinPackingGap.singletonPacking line 90

    Also declared: OAI/Computability/BinPacking/Model.lean:90 (same declaration text).

  17. theorem OAI.BinPackingGap.exists_packing line 103

    Also declared: OAI/Computability/BinPacking/Model.lean:103 (same declaration text).

  18. def OAI.BinPackingGap.opt line 106

    Also declared: OAI/Computability/BinPacking/Model.lean:106 (same declaration text).

  19. def OAI.BinPackingGap.IndividualConfiguration line 110

    Also declared: OAI/Computability/BinPacking/Model.lean:110 (same declaration text).

  20. instance OAI.BinPackingGap.(instance at line 113) line 113
  21. def OAI.BinPackingGap.NumericalSize line 116

    Also declared: OAI/Computability/BinPacking/Model.lean:116 (same declaration text).

  22. instance OAI.BinPackingGap.(instance at line 118) line 118
  23. theorem OAI.BinPackingGap.NumericalSize.positive line 125

    Also declared: OAI/Computability/BinPacking/Model.lean:125 (same declaration text).

    Checked implications (found by the pipeline and checked by Lean's kernel when it ran; a recorded result, not checked again in this build: what these are)

    Gives

  24. def OAI.BinPackingGap.NumericalSize.multiplicity line 130

    Also declared: OAI/Computability/BinPacking/Model.lean:130 (same declaration text).

  25. def OAI.BinPackingGap.NumericalSize.capacityBound line 133

    Also declared: OAI/Computability/BinPacking/Model.lean:133 (same declaration text).

  26. theorem OAI.BinPackingGap.NumericalSize.capacityBound_spec line 136

    Also declared: OAI/Computability/BinPacking/Model.lean:136 (same declaration text).

  27. def OAI.BinPackingGap.TypeConfiguration line 141

    Also declared: OAI/Computability/BinPacking/Model.lean:141 (same declaration text).

  28. theorem OAI.BinPackingGap.TypeConfiguration.count_lt_bound line 148

    Also declared: OAI/Computability/BinPacking/Model.lean:148 (same declaration text).

    Checked implications (found by the pipeline and checked by Lean's kernel when it ran; a recorded result, not checked again in this build: what these are)

    Gives

    • together with OAI.Problem337.egyptian_length_is_minimum, gives ∀ {I : OAI.BinPackingGap.Instance} (c : OAI.BinPackingGap.TypeConfiguration I) (s : OAI.BinPackingGap.NumericalSize I), 1 ≤ ↑c s → (∃ n, OAI.Problem337.IsEgyptianExpansion (↑(↑c s) / ↑s.capacityBound) n) ∧ ∀ (k : ℕ), (∃… (short composition) checked derivation
  29. def OAI.BinPackingGap.TypeConfiguration.boundedCounts line 159

    Also declared: OAI/Computability/BinPacking/Model.lean:159 (same declaration text).

  30. theorem OAI.BinPackingGap.TypeConfiguration.boundedCounts_injective line 162

    Also declared: OAI/Computability/BinPacking/Model.lean:162 (same declaration text).

  31. instance OAI.BinPackingGap.TypeConfiguration.(instance at line 170) line 170
  32. instance OAI.BinPackingGap.TypeConfiguration.(instance at line 174) line 174
  33. def OAI.BinPackingGap.FractionalCover.Feasible line 183

    Also declared: OAI/Computability/BinPacking/Model.lean:183 (same declaration text).

  34. def OAI.BinPackingGap.FractionalCover.objective line 186

    Also declared: OAI/Computability/BinPacking/Model.lean:186 (same declaration text).

  35. def OAI.BinPackingGap.FractionalCover.objectiveSet line 188

    Also declared: OAI/Computability/BinPacking/Model.lean:188 (same declaration text).

  36. def OAI.BinPackingGap.FractionalCover.value line 191

    Also declared: OAI/Computability/BinPacking/Model.lean:191 (same declaration text).

  37. def OAI.BinPackingGap.individualMatrix line 196

    Also declared: OAI/Computability/BinPacking/Model.lean:196 (same declaration text).

  38. def OAI.BinPackingGap.individualLP line 199

    Also declared: OAI/Computability/BinPacking/Model.lean:199 (same declaration text).

  39. def OAI.BinPackingGap.typeMatrix line 202

    Also declared: OAI/Computability/BinPacking/Model.lean:202 (same declaration text).

  40. def OAI.BinPackingGap.typeLP line 205

    Also declared: OAI/Computability/BinPacking/Model.lean:205 (same declaration text).

  41. abbrev OAI.BinPackingGap.RawInstance line 208

    Also declared: OAI/Computability/BinPacking/Model.lean:208 (same declaration text).

  42. abbrev OAI.BinPackingGap.RawReductionOutput line 210

    Also declared: OAI/Computability/BinPacking/Model.lean:210 (same declaration text).

  43. def OAI.BinPackingGap.RawInstance.Valid line 214

    Also declared: OAI/Computability/BinPacking/Model.lean:214 (same declaration text).

  44. def OAI.BinPackingGap.RawInstance.ratValue line 217

    Also declared: OAI/Computability/BinPacking/Model.lean:217 (same declaration text).

  45. theorem OAI.BinPackingGap.RawInstance.den_pos line 219

    Also declared: OAI/Computability/BinPacking/Model.lean:219 (same declaration text).

  46. def OAI.BinPackingGap.RawInstance.toInstance line 222

    Also declared: OAI/Computability/BinPacking/Model.lean:222 (same declaration text).

  47. structure OAI.BinPackingGap.RawPacking line 232

    Also declared: OAI/Computability/BinPacking/Model.lean:232 (same declaration text).

  48. def OAI.BinPackingGap.RawPacking.load line 238

    Also declared: OAI/Computability/BinPacking/Model.lean:238 (same declaration text).

  49. def OAI.BinPackingGap.RawPacking.Feasible line 242

    Also declared: OAI/Computability/BinPacking/Model.lean:242 (same declaration text).

  50. abbrev OAI.BinPackingGap.BinaryEncoding.natBits line 251

    Also declared: OAI/Computability/BinPacking/Model.lean:251 (same declaration text).

  51. abbrev OAI.BinPackingGap.BinaryEncoding.parseNat line 253

    Also declared: OAI/Computability/BinPacking/Model.lean:253 (same declaration text).

  52. def OAI.BinPackingGap.BinaryEncoding.listBits line 255

    Also declared: OAI/Computability/BinPacking/Model.lean:255 (same declaration text).

  53. def OAI.BinPackingGap.BinaryEncoding.pairBits line 259

    Also declared: OAI/Computability/BinPacking/Model.lean:259 (same declaration text).

  54. def OAI.BinPackingGap.BinaryEncoding.optionBits line 262

    Also declared: OAI/Computability/BinPacking/Model.lean:262 (same declaration text).

  55. abbrev OAI.BinPackingGap.BinaryEncoding.Parser line 266

    Also declared: OAI/Computability/BinPacking/Model.lean:266 (same declaration text).

  56. def OAI.BinPackingGap.BinaryEncoding.parsePair line 268

    Also declared: OAI/Computability/BinPacking/Model.lean:268 (same declaration text).

  57. def OAI.BinPackingGap.BinaryEncoding.parseListAux line 274

    Also declared: OAI/Computability/BinPacking/Model.lean:274 (same declaration text).

  58. def OAI.BinPackingGap.BinaryEncoding.parseList line 283

    Also declared: OAI/Computability/BinPacking/Model.lean:283 (same declaration text).

  59. def OAI.BinPackingGap.BinaryEncoding.decode line 286

    Also declared: OAI/Computability/BinPacking/Model.lean:286 (same declaration text).

  60. def OAI.BinPackingGap.BinaryEncoding.rawInstanceBits line 290

    Also declared: OAI/Computability/BinPacking/Model.lean:290 (same declaration text).

  61. def OAI.BinPackingGap.BinaryEncoding.assignmentBits line 293

    Also declared: OAI/Computability/BinPacking/Model.lean:293 (same declaration text).

  62. def OAI.BinPackingGap.BinaryEncoding.rawPackingBits line 295

    Also declared: OAI/Computability/BinPacking/Model.lean:295 (same declaration text).

  63. def OAI.BinPackingGap.BinaryEncoding.packingResultBits line 298

    Also declared: OAI/Computability/BinPacking/Model.lean:298 (same declaration text).

  64. def OAI.BinPackingGap.BinaryEncoding.rawReductionOutputBits line 300

    Also declared: OAI/Computability/BinPacking/Model.lean:300 (same declaration text).

  65. def OAI.BinPackingGap.BinaryEncoding.parseRawInstance line 303

    Also declared: OAI/Computability/BinPacking/Model.lean:303 (same declaration text).

  66. def OAI.BinPackingGap.BinaryEncoding.decodeRawInstance line 305

    Also declared: OAI/Computability/BinPacking/Model.lean:305 (same declaration text).

  67. abbrev OAI.BinPackingGap.BitLanguage line 313

    Also declared: OAI/Computability/BinPacking/Model.lean:311 (same declaration text).

  68. def OAI.BinPackingGap.InP line 315

    Also declared: OAI/Computability/BinPacking/Model.lean:313 (same declaration text).

  69. def OAI.BinPackingGap.ClassP line 322

    Also declared: OAI/Computability/BinPacking/Model.lean:320 (same declaration text).

  70. def OAI.BinPackingGap.ClassNP line 324

    Also declared: OAI/Computability/BinPacking/Model.lean:322 (same declaration text).

  71. def OAI.BinPackingGap.PEqualsNP line 326

    Also declared: OAI/Computability/BinPacking/Model.lean:324 (same declaration text).

  72. structure OAI.BinPackingGap.AbsoluteAdditiveAlgorithm line 328

    Also declared: OAI/Computability/BinPacking/Model.lean:326 (same declaration text).

  73. structure OAI.BinPackingGap.PackingGapReduction line 337

    Also declared: OAI/Computability/BinPacking/Model.lean:335 (same declaration text).

  74. def OAI.BinPackingGap.PackingGapNPHard line 351

    Also declared: OAI/Computability/BinPacking/Model.lean:349 (same declaration text).

  75. theorem OAI.BinPackingGap.main_results Challenge statement: Bin packing and unbounded configuration-LP gaps sorry line 356

    L4DEL explanation

    The formalized results rule out a universal additive bound for the configuration linear program in bin packing. For every integer $c\ge0$, there are an integer $B$ and a rational instance with $5B$ items whose individual-copy and size-type configuration-LP values both equal $B$, but whose integral optimum is greater than $B+c$. Distinguishing a packing in $B$ bins from the absence of one in $B+c$ bins is NP-hard for each fixed $c$. A deterministic polynomial-time algorithm with a fixed absolute additive allowance exists exactly when $P=NP$; under that equality, an optimal algorithm is constructed.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Computability.BinPacking.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Computability/BinPacking/Main.lean:7 (same statement text; different proof or body). Qualify references as OAI.BinPackingGap.main_results@path.

    theorem main_results :
    (∀ c : ℕ, ∃ I : Instance, ∃ B : ℕ,
      I.n = 5 * B ∧
      (∀ i, (1 / 6 : ℚ) < I.size i ∧ I.size i < 1) ∧
      B + c < opt I ∧ individualLP I = (B : ℝ) ∧ typeLP I = (B : ℝ)) ∧
    (∀ c : Nat, PackingGapNPHard c) ∧
    ((∃ c : Nat, Nonempty (AbsoluteAdditiveAlgorithm c)) ↔ PEqualsNP) ∧
    (PEqualsNP → ∃ algorithm : AbsoluteAdditiveAlgorithm 0,
    (∀ (items : RawInstance) (valid : items.Valid), ∃ packing : RawPacking,
      algorithm.run (BinaryEncoding.rawInstanceBits items) = some packing ∧
      packing.Feasible items ∧ packing.bins = opt (items.toInstance valid)) ∧
    algorithm.run (BinaryEncoding.rawInstanceBits []) = some ⟨0, []⟩ ∧
…

    Mentions: OAI.BinPackingGap.Instance, OAI.BinPackingGap.opt, OAI.BinPackingGap.individualLP, OAI.BinPackingGap.typeLP, OAI.BinPackingGap.PackingGapNPHard, OAI.BinPackingGap.AbsoluteAdditiveAlgorithm, OAI.BinPackingGap.PEqualsNP, OAI.BinPackingGap.RawInstance, OAI.BinPackingGap.RawPacking, OAI.BinPackingGap.BinaryEncoding.rawInstanceBits