three_sum_lower_bound
Proved⚠️ Retired — incorrect formalization
The Lean statement below does not express the result
three_sum_lower_boundis named for, so itsProvedstatus carries no information about it. Do not import it or use it as a dependency.
3SUM conjecture: The 3SUM problem (does a set of n integers contain three elements summing to 0?) cannot be solved in o(n²) time in the algebraic decision tree model. Evidence: no sub-quadratic algorithm known. Gajentaan–Sharir (1995) showed many problems are 3SUM-hard. Resolution would have major algorithmic consequences.
Why this node was retired
The posted statement is
import Mathlib
theorem three_sum_lower_bound :
∀ (algo : List ℤ → Bool),
(∀ L : List ℤ, algo L = true ↔ ∃ a ∈ L, ∃ b ∈ L, ∃ c ∈ L, a + b + c = 0) →
∀ n : ℕ, ∃ (L : List ℤ) (_ : L.length = n), True := by
sorry
The conclusion is ∀ n, ∃ (L : List ℤ) (_ : L.length = n), True, satisfied by any list of length n. The hypothesis characterising algo is never used, and no running-time model, cost measure or lower bound appears anywhere.
What a faithful statement would require
A cost model for the algorithm is needed, together with a conclusion bounding its cost from below on some input of each size.
No corrected replacement node exists yet.
import Mathlib
import Mathlib
theorem three_sum_lower_bound :
∀ (algo : List ℤ → Bool),
(∀ L : List ℤ, algo L = true ↔ ∃ a ∈ L, ∃ b ∈ L, ∃ c ∈ L, a + b + c = 0) →
∀ n : ℕ, ∃ (L : List ℤ) (_ : L.length = n), True := by
sorry