Prove ParityLifts (openai/math family 133: The complexity of Weisfeiler–Leman refinement) in Lean 4 with…
Prove ParityLifts (openai/math family 133: The complexity of Weisfeiler–Leman refinement) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 133 of the release, The complexity of Weisfeiler–Leman refinement (Theoretical…
The task
Context: this statement belongs to family 133 of the release, *The complexity of Weisfeiler–Leman refinement* (Theoretical computer science). The family as a whole: Proves unconditional $n^{\Omega(k)}$ deterministic time lower bounds for joint and separate $k$-dimensional Weisfeiler–Leman equivalence, for…
Part of raising-heart/openai-math.