Browse › Theoretical computer science › 133 The computational complexity of Weisfeiler–Leman refinement
Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Radu Curticapean, Mingjun Liu, Daniel Neuen, and Tim Seppelt, Lower Bounds for Weisfeiler–Leman (Zenodo:10.5281/zenodo.23213174, 2026-10-07). This concurrent AI-assisted manuscript cites the paper and states EXPTIME- and XP-completeness for pair equivalence on simple bipartite 3-degenerate graphs; its preface dates the AI-assisted results to September 19–29 and describes the manuscript as a hastily written public timestamp. [AI-generated per source] [family-level]
Formalization
- OpenAI, The computational complexity of Weisfeiler–Leman refinement: Lean scope notes (OpenAI Math Release, lean/docs/133.md, 2026-10-06). The release's Lean scope note says EXPTIME-completeness of joint-update $k$-WL equivalence with binary $k\ge2$ is formalized, for general graphs and for connected equal-order simple uncolored graphs of maximum degree three, with comparator
VariableWL.lean. [AI-generated per source] [family-level] - OpenAI, lean/OAI/Combinatorics/VariableWL/Completeness.lean (openai/math, commit adc7f12, 2026). The release's Lean file containing
theorem main : EXPTIMEComplete WL ∧ EXPTIMEComplete SubWL, the formal counterpart of the paper's Theorem 1.1. - Radu Curticapean, Mingjun Liu, Daniel Neuen, and Tim Seppelt, Lean formalizations of Weisfeiler–Leman results (supplement to Zenodo:10.5281/zenodo.23213174, 2026-10-07). The archive documents WL/game/homomorphism correspondence, round bounds and a deterministic register compiler, with decision-complexity reductions outside its scope. [AI-generated per source] [family-level]
Related prior literature mentioned by others
- Martin Grohe, Moritz Lichter, Daniel Neuen, and Pascal Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements (arXiv:2308.11970v2, 2025-01-27; Journal of the ACM 72(3), 2025). Curticapean and coauthors cite its Ω(n^{k/2}) refinement-round bound as a predecessor to their concurrent work on this family. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Phokion G. Kolaitis and Jonathan Panttaja, On the Complexity of Existential Pebble Games (CSL 2003, LNCS, pp. 314–329, doi:10.1007/978-3-540-45220-1_26). According to later citations, this work shows that deciding the existential $k$-pebble game is EXPTIME-complete when $k$ is part of the input, the existential-game analogue of the paper's Theorem 1.1 for the bijective game.
Digests and expositions
- Orply / Perplexity, Weisfeiler–Leman Equivalence Remains EXPTIME-Complete on Subcubic Graphs (Orply, 2026-10-11). This explicitly AI-assisted exposition outlines joint refinement, dimension capping, the bijective game and the subcubic construction, while stating that it omits full proofs. [AI-generated per source]
News and blogs
- Tim Seppelt, News: Lower Bounds for Weisfeiler–Leman (author website, 2026-10-07). Seppelt announces the concurrent manuscript in response to OpenAI’s release and reports extensions involving classical complexity, parameterized complexity and iteration bounds. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 133
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/133.md. The Lean statements have not been checked by people against the paper's claims.
Family 133: The computational complexity of Weisfeiler–Leman refinement
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.
Other papers in this family:
- Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence · September 25, 2026
- The complexity of identifying a graph by Weisfeiler–Leman refinement · September 25, 2026
- Unconditional time lower bounds for Weisfeiler–Leman equivalence · September 25, 2026