The distinct-position 3SUM problem

This is the input predicate of Anthropic's pinned end statement, without its source machine or running-time convention. Equal values at different positions are allowed. In particular, three occurrences of zero are a solution, whereas one occurrence is not.

Main definitions

• HasSolution: three distinct input positions whose integer values sum to zero.

def Cslib.Algorithms.ThreeSum.HasSolution {n : ℕ} (x : Fin n → ℤ) : Prop

3SUM on an integer array, requiring three different positions. Values may repeat.