Berkholz's question: is Weisfeiler-Leman equivalence with the dimension as part of the input EXPTIME-complete?

The $k$ -dimensional Weisfeiler-Leman algorithm repeatedly refines colours of $k$ -tuples of vertices; two graphs are $k$ -WL equivalent if their stable colour histograms agree. For fixed $k$ this takes time $n^{O(k)}$ , so with $k$ given in binary the equivalence problem lies in EXPTIME. Seppelt (MFCS 2024), and independently Lichter, Rassmann and Schweitzer, proved it coNP-hard when $k$ is part of the input, and Seppelt recorded Christoph Berkholz's question whether it is in fact EXPTIME-complete. Given two graphs by adjacency matrices and a dimension $k\ge2$ in binary, is deciding $k$ -WL equivalence EXPTIME-complete?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Computational complexity; graph isomorphism and finite model theory
Posed by: Christoph Berkholz, as recorded by Tim Seppelt (MFCS 2024, the question preceding Theorem 5)
Year posed: 2024
Years open: 2y
Solved: 2026-09-25
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 15 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1 (principal manuscript): deciding joint-update $k$ -WL equivalence with $k\ge2$ in binary and explicit adjacency matrices is EXPTIME-complete under polynomial-time many-one reductions, also for connected simple uncoloured graphs of equal order and maximum degree three. Companions claim: deciding whether a given dimension identifies a graph (WL dimension at most $k$ ) is EXPTIME-complete, also with $k$ in unary; for every large fixed $k$ , deciding $k$ -WL equivalence needs $n^{\Omega(k)}$ deterministic sequential time unconditionally (multitape Turing machines and log-word RAMs, diameter-two graphs); and parity lifts give $n^{\Omega(k)}$ exclusions under ETH. No randomized or nonuniform lower bounds are claimed, and the separate-update convention is treated only in the fixed-dimension companions.

What the AI did

The release README says all results in the release were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This family is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. The family has four manuscripts of the same date sharing a compressed-computation construction: the principal one (variable-dimension equivalence), graph identification with dimension in the input, unconditional fixed-dimension time lower bounds, and parity lifts with ETH-based exclusions. All four main statements are formalized in Lean.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 and the history section of the principal manuscript were read against Berkholz's question as Seppelt records it. Lean: lean/docs/133.md links ComparatorChallenges/VariableWL (theorem OAI.VariableWL.main, solution module OAI.Combinatorics.VariableWL.Completeness, file exists at the pinned commit), not in formalization.yaml. The statement was read: with Turing machines, EXPTIME and polynomial-time many-one reductions defined from scratch, both the language of (G, H, k) with k >= 2 in binary and joint-update k-WL equivalence, and its connected subcubic equal-order restriction, are EXPTIME-complete. That is the headline. Not rebuilt here. The result uses the joint-update convention.

Berkholz's question: is Weisfeiler-Leman equivalence with the dimension as part of the input EXPTIME-complete?

What was actually shown

What the AI did

Verification

Sources

Discussion