`ComparatorChallenges/OptimalMaxCut.lean`

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

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

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

25 declarations, 1 contain sorry, 0 declared as axioms

structure OAI.MaxCutGames.BinaryFormula.Literal line 7
Also declared: OAI/Computability/MaxCut/Model.lean:7 (same declaration text).
def OAI.MaxCutGames.BinaryFormula.Literal.eval line 12
Also declared: OAI/Computability/MaxCut/Model.lean:12 (same declaration text).
abbrev OAI.MaxCutGames.BinaryFormula.Clause line 15
Also declared: OAI/Computability/MaxCut/Model.lean:15 (same declaration text).
def OAI.MaxCutGames.BinaryFormula.Clause.eval line 17
Also declared: OAI/Computability/MaxCut/Model.lean:17 (same declaration text).
structure OAI.MaxCutGames.BinaryFormula.Formula An ordinary conjunction of three-slot clauses with sparse variable names line 22
Source documentation
An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.
L4DEL explanation
An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:22 (same declaration text).
```
structure Formula where
…
```
def OAI.MaxCutGames.BinaryFormula.Formula.Satisfiable line 25
Also declared: OAI/Computability/MaxCut/Model.lean:25 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.bitsValue line 34
Also declared: OAI/Computability/MaxCut/Model.lean:34 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.frame Prefix-free framing on the two-symbol input alphabet line 39
Source documentation
Prefix-free framing on the two-symbol input alphabet.
L4DEL explanation
Prefix-free framing on the two-symbol input alphabet.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:39 (same declaration text).
```
def frame : List Bool → List Bool
  | [] => [false]
  | b :: bits => true :: b :: frame bits
```
def OAI.MaxCutGames.BinaryEncoding.parseFrame line 43
Also declared: OAI/Computability/MaxCut/Model.lean:43 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.nameBits line 50
Also declared: OAI/Computability/MaxCut/Model.lean:50 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.parseName Equality with the canonical digits rejects alternate padded encodings line 53
Source documentation
Equality with the canonical digits rejects alternate padded encodings.
L4DEL explanation
Equality with the canonical digits rejects alternate padded encodings.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:53 (same declaration text).
```
def parseName (input : List Bool) : Option (Nat × List Bool) := do
…
```
def OAI.MaxCutGames.BinaryEncoding.parseLiteral line 58
Also declared: OAI/Computability/MaxCut/Model.lean:58 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.parseClause line 64
Also declared: OAI/Computability/MaxCut/Model.lean:64 (same declaration text).
def OAI.MaxCutGames.BinaryEncoding.parseClauses Fuel bounds the number of clause iterations, not the size of any name line 71
Source documentation
Fuel bounds the number of clause iterations, not the size of any name.
L4DEL explanation
Fuel bounds the number of clause iterations, not the size of any name.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:71 (same declaration text).
```
def parseClauses : Nat → List Bool → Option (List Clause × List Bool)
  | 0, _ => none
  | _ + 1, false :: rest => some ([], rest)
  | fuel + 1, true :: input => do
      let (clause, input) ← parseClause input
      let (clauses, rest) ← parseClauses fuel input
      return (clause :: clauses, rest)
  | _ + 1, [] => none
```
Mentions: OAI.MaxCutGames.BinaryEncoding.parseClause
def OAI.MaxCutGames.BinaryEncoding.decodeFormula line 80
Also declared: OAI/Computability/MaxCut/Model.lean:80 (same declaration text).
def OAI.OptimalMaxCut.alphaGW The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1 line 91
Source documentation
The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1.
L4DEL explanation
The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:91 (same declaration text).
```
noncomputable def alphaGW : ℝ :=
…
```
def OAI.OptimalMaxCut.binary3SAT The ordinary binary 3SAT language, including rejection of malformed words line 96
Source documentation
The ordinary binary 3SAT language, including rejection of malformed words.
L4DEL explanation
The ordinary binary 3SAT language, including rejection of malformed words.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:96 (same declaration text).
```
def binary3SAT (input : List Bool) : Prop :=
…
```
structure OAI.OptimalMaxCut.Graph A finite simple unweighted graph with its full Boolean adjacency table line 101
Source documentation
A finite simple unweighted graph with its full Boolean adjacency table.
L4DEL explanation
A finite simple unweighted graph with its full Boolean adjacency table.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:101 (same declaration text).
```
structure Graph where
…
```
def OAI.OptimalMaxCut.Graph.cutSize Each unordered distinct edge crossing the cut is counted exactly once line 108
Source documentation
Each unordered distinct edge crossing the cut is counted exactly once.
L4DEL explanation
Each unordered distinct edge crossing the cut is counted exactly once.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:108 (same declaration text).
```
def Graph.cutSize (G : Graph) (cut : Fin G.vertices → Bool) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Graph
def OAI.OptimalMaxCut.Graph.maxCut The maximum over all Boolean cuts of the finite vertex set line 113
Source documentation
The maximum over all Boolean cuts of the finite vertex set.
L4DEL explanation
The maximum over all Boolean cuts of the finite vertex set.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:113 (same declaration text).
```
def Graph.maxCut (G : Graph) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Graph
structure OAI.OptimalMaxCut.ScaledGraph The positive integer scale Q is part of the output line 118
Source documentation
The positive integer scale Q is part of the output. It need not equal the number of graph edges.
L4DEL explanation
The positive integer scale Q is part of the output. It need not equal the number of graph edges.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:118 (same declaration text).
```
structure ScaledGraph where
…
```
def OAI.OptimalMaxCut.ScaledGraph.bits Canonical delimited binary vertex count and scale, followed by the full adjacency table in lexicographic order line 125
Source documentation
Canonical delimited binary vertex count and scale, followed by the full adjacency table in lexicographic order.
L4DEL explanation
Canonical delimited binary vertex count and scale, followed by the full adjacency table in lexicographic order.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:125 (same declaration text).
```
def ScaledGraph.bits (G : ScaledGraph) : List Bool :=
…
```
Mentions: OAI.OptimalMaxCut.ScaledGraph
structure OAI.OptimalMaxCut.GapReduction The rational gap bounds and the finite machine are fixed before the input line 133
Source documentation
The rational gap bounds and the finite machine are fixed before the input. The bounds compare the maximum cut divided by the positive output scale.
L4DEL explanation
The rational gap bounds and the finite machine are fixed before the input. The bounds compare the maximum cut divided by the positive output scale.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Computability/MaxCut/Model.lean:133 (same declaration text).
```
structure GapReduction (α : ℝ) where
…
```
def OAI.OptimalMaxCut.MainStatement line 148
Also declared: OAI/Computability/MaxCut/Model.lean:148 (same declaration text).
theorem OAI.OptimalMaxCut.main Challenge statement: Optimal Max-Cut hardness gap sorry line 153
L4DEL explanation
This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.
1. The linked formalization note covers 5 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
2. The repository's comparator configuration selects OAI.Computability.MaxCut.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Computability/MaxCut/Main.lean:53 (different declaration text). Qualify references as OAI.OptimalMaxCut.main@path.
```
theorem OptimalMaxCut.main : OptimalMaxCut.MainStatement := by
…
```
Mentions: OAI.OptimalMaxCut.MainStatement