View source for The computational complexity of Weisfeiler–Leman refinement

The '''computational complexity of Weisfeiler–Leman refinement''' concerns how hard it is to decide whether two graphs are indistinguishable by ''k''-dimensional Weisfeiler–Leman refinement, which colours ''k''-tuples of vertices by repeatedly recording their local extension patterns. Four manuscripts dated 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claim an unconditional ''n''<sup>Ω(''k'')</sup> time lower bound for fixed large ''k'', and EXPTIME-completeness when the dimension is part of the input. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript ''Unconditional time lower bounds for Weisfeiler–Leman equivalence'':
** For each fixed dimension ''k'', stabilization of the refinement gives an algorithm with running time ''n''<sup>''O''(''k'')</sup>; the question is whether a growing exponent is necessary for every sequential algorithm deciding the equivalence, not only for refinement itself.
** Cai, Fürer and Immerman established fundamental limits of bounded-variable graph identification through parity constructions. Grohe, Lichter, Neuen and Schweitzer proved that some graph families need Ω<sub>''k''</sub>(''n''<sup>''k''/2</sup>) rounds of ''k''-dimensional refinement; round bounds concern the refinement process, not every decider.
** With the dimension as part of the input, Seppelt and, independently, Lichter, Raßmann and Schweitzer proved coNP-hardness of deciding equivalence of a supplied pair. For existential pebble games, Berkholz proved unconditional time lower bounds with exponent linear in the number of pebbles.

== The original results ==
* '''Fixed-dimension lower bound.''' Theorem 1.1 of ''Unconditional time lower bounds for Weisfeiler–Leman equivalence'' states that there are absolute constants ''c'' &gt; 0 and ''k''<sub>0</sub> such that for every fixed ''k'' ≥ ''k''<sub>0</sub>, every deterministic decider of ''k''-dimensional Weisfeiler–Leman equivalence needs time at least ''n''<sup>''ck''</sup> on ''n''-vertex inputs for all large ''n''. The bound is stated for multitape Turing machines and for sequential random-access machines with logarithmic word length, for explicit adjacency-matrix inputs, without any complexity assumption, and even for simple connected uncolored graphs of diameter at most two. It covers both the joint and the separate replacement conventions.
* '''Dimension as part of the input.''' ''Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs'' states that deciding joint-update ''k''-dimensional equivalence is EXPTIME-complete when ''k'' ≥ 2 is encoded in binary, even for connected graphs of maximum degree three. ''The complexity of identifying a graph by Weisfeiler–Leman refinement'' states that deciding whether refinement of a given dimension distinguishes a graph from every non-isomorphic graph is EXPTIME-complete.
* '''Parity lifts.''' ''Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence'' constructs, for ''k'' ≥ 4, pairs of graphs that are ''k''-dimensionally equivalent exactly when a finite choice system has no compatible choice, and derives conditional time exclusions under a form of the Exponential Time Hypothesis.
* '''Sources.''' At commit <code>1581d4c</code>, for example [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026 Unconditional time lower bounds for Weisfeiler–Leman equivalence]; the four manuscripts are listed in the scope note below.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/133.md lean/docs/133.md] states that the Lean formalization proves the parity-lift characterization, the EXPTIME-completeness of identification, the unconditional fixed-dimension time lower bound and the EXPTIME-completeness of variable-dimension equivalence. It states that the paper's conditional running-time exclusions are outside the formal statements. The Comparator challenges are <code>ParityLifts</code>, <code>WLIdentification</code>, <code>WeisfeilerLeman</code> and <code>VariableWL</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 23 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>bb5fdb6</code>, 18 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records sandboxed Comparator passes for all four challenges. Its notes list the hand-built computation models among the definitions to check: a multitape Turing machine and a logarithmic-word random-access machine in which a whole word operation implemented by a Turing machine within a polynomial bound counts as one instruction. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || cert-machine, openai/math lane K: run 38051470892 for [https://github.com/carlostoledo1891/cert-machine/blob/61aae8eb42f1967e16d37d78cfe8a5c1be6d0d72/corpus/openai-math/kernel-runs/38051470892/ParityLifts.json ParityLifts], [https://github.com/carlostoledo1891/cert-machine/blob/61aae8eb42f1967e16d37d78cfe8a5c1be6d0d72/corpus/openai-math/kernel-runs/38051470892/WLIdentification.json WLIdentification], [https://github.com/carlostoledo1891/cert-machine/blob/61aae8eb42f1967e16d37d78cfe8a5c1be6d0d72/corpus/openai-math/kernel-runs/38051470892/WeisfeilerLeman.json WeisfeilerLeman] and [https://github.com/carlostoledo1891/cert-machine/blob/61aae8eb42f1967e16d37d78cfe8a5c1be6d0d72/corpus/openai-math/kernel-runs/38051470892/VariableWL.json VariableWL] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept all four solutions, in 146 s to 405 s each. || Repository.
|-
| 2026-10-22 (latest commit) || [https://github.com/jiamo/lambda-computability/tree/f5d24ca31a707e55067dddb36e24082fe21227db jiamo/lambda-computability] (GitHub, commit <code>f5d24ca</code>) || Use (Lean port) || A Lean library on lambda calculus and computability. Its <code>NOTICE</code> file lists the collection's <code>WeisfeilerLeman</code> directory, 43 files, as adapted to its own Lean and Mathlib versions, and states that "the mathematics and the proofs are upstream's". || GitHub repository.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]