OpenAI claim summary for CS-175
computer sciencemathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 133; 2026-09-25).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Parity witnesses for Weisfeiler–Leman equivalence
OpenAI's claim
OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 133; 2026-09-25), the asserted result is that compatible-choice systems can be encoded by graph pairs whose fixed-dimensional WL equivalence is exactly absence of a successful choice, with specified early-round detection and conditional ETH consequences.Mathematical statement of the claimed result
Manuscript 1.
Fix $k\ge4$ and put $t=k+1$ for joint correlated-replacement $k$-WL, or $t=k$ for separate-coordinate refinement. A choice system has exactly $t$ finite domains $D_1,\ldots,D_t$ and pairwise label maps $\lambda_{ij}^i:D_i\to L_{ij}$, $\lambda_{ij}^j:D_j\to L_{ij}$. A successful choice satisfies $\lambda_{ij}^i(d_i)=\lambda_{ij}^j(d_j)$ for every pair. The claimed explicit uncolored simple graphs of equal order satisfy \[ X_0\equiv_kX_{\star}\quad\Longleftrightarrow\quad\text{there is no successful choice}. \] Both common-color separate comparison and pure-tuple comparison within a disjoint union are allowed. If all domain and label sets have size at most $A\ge1$, the common graph order is bounded by \[ A\left(t2^{t-2+3\binom{t-1}{2}}+12\binom t3\right). \] If a successful choice exists, the histograms disagree by round two in the joint convention and by round one in the separate convention.Outline of the argument
For manuscript 1 (family 133; 2026-09-25), homogeneous and affine parity lifts share a typed base graph. A dual parity certificate compares their lift counts, and bounded-treewidth homomorphism witnesses recover a compatible choice, making the refinement dimension track the number of domains.Formal verification
For manuscript 1 (family 133; 2026-09-25), the documented Lean scope is the parity-lift construction and its early-round WL detection, for both refinement conventions; the conditional ETH time exclusions are not among those selected statements.The selected statement includes the clause used for this problem.
The linked family Comparator checks are ParityLifts.lean, VariableWL.lean, WLIdentification.lean, WeisfeilerLeman.lean.
Their named declarations include OAI.ParityWL.parity_reduction, OAI.VariableWL.main, OAI.WLIdentification.main, OAI.WLTime.unconditional_time_lower_bound.
This site has not executed the Lean code. Described statement coverage is not an independent proof check.
Status caveat
The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.Sources
- OpenAI, Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence, 2026-09-25; citation key
OAI:Parity-lifts-and-bounded-treewidth-witnesses-for-Weisfeiler-Leman-equivalence-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:choice-reduction. - Family 133: Lean scope.
- Comparator ParityLifts.json.
- Comparator ParityLifts.lean.
- Comparator VariableWL.json.
- Comparator VariableWL.lean.
- Comparator WLIdentification.json.
- Comparator WLIdentification.lean.
- Comparator WeisfeilerLeman.json.
- Comparator WeisfeilerLeman.lean.
- OpenAI catalogue entry.