EXPTIME-completeness of variable-dimensional WL

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.