we-solve (beta)

CS-134 · computer science · mathematics · Computational complexity

Unconditional time lower bounds for fixed-dimensional WL

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Are there $c>0,k_{0}$ such that, for every fixed $k\geq k_{0}$, every correct deterministic decider of k-WL equivalence has worst-case time at least $n^{ck}$ for every sufficiently large n, even on connected simple uncolored graphs of diameter $\leq 2$, for both joint and separate refinement on multitape machines or the specified sequential logarithmic-word RAM?

Short English statement

Are there $c>0,k_{0}$ such that, for every fixed $k\geq k_{0}$, every correct deterministic decider of k-WL equivalence has worst-case time at least $n^{ck}$ for every sufficiently large n, even on connected simple uncolored graphs of diameter $\leq 2$, for both joint and separate refinement on multitape machines or the specified sequential logarithmic-word RAM?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-134-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-134

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 133; 2026-09-25).

Unconditional time lower bounds for fixed-dimensional WL

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 133; 2026-09-25), the asserted result is that sufficiently large fixed WL dimension $k$ needs deterministic sequential time $n^{\Omega(k)}$ on some graphs at every large order, without a complexity assumption.

Mathematical statement of the claimed result

Manuscript 1.
For a deterministic decider $A$ of fixed-$k$ Weisfeiler--Leman equivalence, let $T_A(n)$ be its worst running time on pairs of graphs with $n$ vertices each. The claimed lower bound has quantifiers \[ \exists c>0,k_0\ \forall k\ge k_0\ \forall A\text{ correct for }k\text{-WL} \ \exists n_0(A,k)\ \forall n\ge n_0(A,k):\quad T_A(n)\ge n^{ck}. \] It applies to multitape Turing machines and sequential RAMs with $O(\log(n+2))$-bit words and addresses, with each instruction accessing only a bounded number of cells and having polynomial bit complexity as a function of word length. The same bound holds when correctness is required only for graphs that are simple, uncolored and connected, with diameter bounded by two. Both joint coordinate-replacement multisets and separate coordinate-replacement multisets are covered.

Outline of the argument

For manuscript 1 (family 133; 2026-09-25), short consistency instances encode padded computations and are realized by locally translated graph blocks. Exact offset projection gives the bijective-game equivalence, and an every-length diagonal language transfers through controlled padding to connected diameter-two graphs.

Formal verification

For manuscript 1 (family 133; 2026-09-25), OpenAI lists Lean statements for this assertion: sufficiently large fixed WL dimension $k$ needs deterministic sequential time $n^{\Omega(k)}$ on some graphs at every large order, without a complexity assumption.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are ParityLifts.lean, VariableWL.lean, WLIdentification.lean, WeisfeilerLeman.lean.

Their named declarations include OAI.ParityWL.parity_reduction, OAI.VariableWL.main, OAI.WLIdentification.main, OAI.WLTime.unconditional_time_lower_bound.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →