OpenAI claim summary for CS-134
computer sciencemathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
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).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
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
- OpenAI, Unconditional time lower bounds for Weisfeiler–Leman equivalence, 2026-09-25; citation key
OAI:Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 133: Lean scope.
- Comparator ParityLifts.json.
- Comparator ParityLifts.lean.
- Comparator VariableWL.json.
- Comparator VariableWL.lean.
- Comparator WLIdentification.json.
- Comparator WLIdentification.lean.
- Comparator WeisfeilerLeman.json.
- Comparator WeisfeilerLeman.lean.
- OpenAI catalogue entry.