Theoretical computer science · Result 133

The computational complexity of Weisfeiler–Leman refinement

4 papersLean

Proves unconditional \(n^{\Omega(k)}\) deterministic time lower bounds for joint and separate k-dimensional Weisfeiler–Leman equivalence, for sufficiently large fixed k in the specified sequential adjacency-matrix models. With dimension as input, joint equivalence is EXPTIME-complete even on subcubic graphs; deciding whether refinement identifies a graph is also EXPTIME-complete.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 4

Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence

OpenAI · September 25, 2026

For k ≥ 4, we construct two uncolored graphs that are k-dimensional Weisfeiler–Leman equivalent exactly when a prescribed finite-domain choice system has no compatible choice. The system has \(k+1\) domains for joint refinement and k for separate-coordinate refinement. A successful choice is detected after two joint rounds or one separate round. Applied to sparse satisfiability, the reduction gives fixed-dimension \(n^{\Omega(k)}\) time exclusions under positive-rate ETH, even for deciding equality of these early histograms.

Read PDF Download Source

Cite

@misc{OAI:Parity-lifts-and-bounded-treewidth-witnesses-for-Weisfeiler-Leman-equivalence-September-25-2026,
  author = {{OpenAI}},
  title = {{Parity lifts and bounded-treewidth witnesses for Weisfeiler--Leman equivalence}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Parity-lifts-and-bounded-treewidth-witnesses-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf}{OAI:Parity-lifts-and-bounded-treewidth-witnesses-for-Weisfeiler-Leman-equivalence-September-25-2026}},
  year = {2026}
}

The complexity of identifying a graph by Weisfeiler–Leman refinement

OpenAI · September 25, 2026

We prove that deciding whether Weisfeiler–Leman refinement of an input dimension identifies a given graph is EXPTIME-complete. The input is a nonempty finite simple uncolored graph in adjacency-matrix form and a positive binary-encoded dimension. Identification quantifies over every comparison graph.

Read PDF Download Source

Cite

@misc{OAI:The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026,
  author = {{OpenAI}},
  title = {{The complexity of identifying a graph by Weisfeiler--Leman refinement}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf}{OAI:The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026}},
  year = {2026}
}

Unconditional time lower bounds for Weisfeiler–Leman equivalence

OpenAI · September 25, 2026

For every sufficiently large fixed k, deciding whether two n-vertex graphs are k-Weisfeiler–Leman equivalent requires \(n^{\Omega(k)}\) deterministic sequential time in the worst case. The bound holds at every sufficiently large graph order, even for simple connected uncolored graphs of diameter at most two, without a complexity assumption. Inputs are explicit adjacency matrices; the models are multitape Turing machines and sequential logarithmic-word RAMs with fixed polynomial-bit-time instructions. Both joint and separate replacement conventions are covered.

Read PDF Download Source

Cite

@misc{OAI:Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026,
  author = {{OpenAI}},
  title = {{Unconditional time lower bounds for Weisfeiler--Leman equivalence}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf}{OAI:Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026}},
  year = {2026}
}

Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs

OpenAI · September 25, 2026

Deciding joint-update k-dimensional Weisfeiler–Leman equivalence is \(\mathsf{EXPTIME}\)-complete when the two graphs are given by explicit adjacency matrices and k ≥ 2 is encoded in binary. The result holds even for connected simple uncolored graphs of equal positive order and maximum degree at most three.

Read PDF Download Source

Cite

@misc{OAI:Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026,
  author = {{OpenAI}},
  title = {{Variable-dimension Weisfeiler--Leman equivalence on general and subcubic graphs}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf}{OAI:Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization gives the paper's parity-lift graph construction for every Weisfeiler–Leman dimension \(k\ge4\), under both joint and separate conventions. From a finite choice system it constructs two equal-size uncolored graphs that are Weisfeiler–Leman equivalent exactly when the system has no successful compatible choice. The same equivalence holds for the pure variant.

A successful choice is detected by the specified early round: round two in the joint convention and round one in the separate convention. The graph-size bound is linear in the choice-system size with a factor depending on \(k\). The paper's conditional running-time exclusions are outside these selected construction statements.

The formalization proves that deciding whether Weisfeiler–Leman refinement of a supplied dimension identifies a graph is EXPTIME-complete under polynomial-time many-one reductions. The input is a nonempty finite simple uncolored graph encoded by its adjacency matrix together with a positive binary-encoded dimension. Identification quantifies over every comparison graph, and the statement includes both the exponential-time upper bound and hardness.

The formalization proves an unconditional deterministic time lower bound for deciding \(k\)-dimensional Weisfeiler–Leman equivalence. For every sufficiently large fixed \(k\), every deciding algorithm in the stated multitape Turing-machine or sequential logarithmic-word RAM model requires at least \(n^{ck}\) worst-case time for all sufficiently large graph orders \(n\), for one absolute \(c>0\).

The bound covers both joint and separate replacement conventions and remains valid for explicit adjacency-matrix inputs restricted to simple connected uncolored graphs of diameter at most two.

The formalization proves EXPTIME-completeness of deciding joint-update \(k\)-dimensional Weisfeiler–Leman equivalence when \(k\ge2\) is part of the input in binary and the graphs are encoded by explicit adjacency matrices. It proves both the general result and the restriction to connected simple uncolored graphs of equal positive order and maximum degree at most three. Completeness uses polynomial-time many-one reductions.

Comparator links

Result	Comparator statement
Parity-lift characterization of Weisfeiler–Leman equivalence	ParityLifts.lean
EXPTIME-completeness of Weisfeiler–Leman graph identification	WLIdentification.lean
Unconditional sequential time lower bounds for Weisfeiler–Leman equivalence	WeisfeilerLeman.lean
EXPTIME-completeness of variable-dimension Weisfeiler–Leman equivalence	VariableWL.lean

Scope note on GitHub →