OpenAI claim summary for CS-171
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
EXPTIME-completeness of variable-dimensional WL
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 deciding joint-update WL equivalence with binary dimension is EXPTIME-complete even for connected simple uncolored subcubic graph pairs.Mathematical statement of the claimed result
Manuscript 1.
Let $\operatorname{WL}$ consist of triples $(G,H,k)$ with $k\ge2$ in binary and finite simple uncolored graphs in adjacency-matrix encoding, for which joint $k$-dimensional Weisfeiler--Leman refinement gives the same color histogram on the two graphs at every round. Let $\operatorname{SubWL}$ impose the additional conditions that $G,H$ are connected, have the same positive order, and have maximum degree at most three. The claim is \[ \operatorname{WL}\text{ and }\operatorname{SubWL}\text{ are EXPTIME-complete} \] under deterministic polynomial-time many-one reductions. Dimension is part of the input, rather than fixed outside the decision problem.Outline of the argument
For manuscript 1 (family 133; 2026-09-25), homogeneous and affine block equations admit shared readouts and exact local extension. Channels and prefix forests convert the blocks to maximum degree three, while one common block offset supplies an entire announced bijection rather than only a point response.Formal verification
For manuscript 1 (family 133; 2026-09-25), OpenAI lists Lean statements for this assertion: deciding joint-update WL equivalence with binary dimension is EXPTIME-complete even for connected simple uncolored subcubic graph pairs.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, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, 2026-09-25; citation key
OAI:Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - 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.