The computational complexity of Weisfeiler–Leman refinement
From OpenAI Aftermath
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 (github.com/openai/math) claim an unconditional nΩ(k) 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 nO(k); 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 Ωk(nk/2) 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 > 0 and k0 such that for every fixed k ≥ k0, every deterministic decider of k-dimensional Weisfeiler–Leman equivalence needs time at least nck 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
1581d4c, for example 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 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
ParityLifts,WLIdentification,WeisfeilerLemanandVariableWL.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 23 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit bb5fdb6, 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 ParityLifts, WLIdentification, WeisfeilerLeman and 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) | jiamo/lambda-computability (GitHub, commit f5d24ca) |
Use (Lean port) | A Lean library on lambda calculus and computability. Its NOTICE file lists the collection's WeisfeilerLeman 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.
