Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Truly subquadratic 3SUM

Lax350013.ThreeSUM · concepts/Lax350013/ThreeSUM.lean · lax-350013

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Given nn polynomially bounded integers, a deterministic word-RAM program decides whether three distinct positions contain numbers summing to zero in O(n1.9992)O(n^{1.9992}) steps (Theorem 22, using Corollary 26).

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Lax350013.PolynomialTime
    15
    16/-!
    17---
    18title: Truly subquadratic 3SUM
    19type: theorem
    20---
    21Given nn polynomially bounded integers, a deterministic word-RAM program decides whether three distinct positions contain numbers summing to zero in O(n1.9992)O(n^{1.9992}) steps (Theorem 22, using Corollary 26).
    22-/
    23
    24namespace Lax350013.ThreeSUM
    25
    26open Lax350013.PolynomialTime
    27
    28/-- Section 1: «Given n numbers, decide whether three of them sum to 0». Three different positions. -/
    29def ThreeSum : Problem where
    30 Instance n := Fin n → Int
    31 input x := List.ofFn x
    32 yes x := ∃ i j k, i ≠ j ∧ j ≠ k ∧ i ≠ k ∧ x i + x j + x k = 0
    33
    34/-- Theorem 22: «solve 3SUM on n integers of absolute value at most n^ν», in time «O(n^1.9992)». -/
    35def Theorem_22_3SUM : Prop :=
    36 ThreeSum.SolvedInTime 1.9992
    37
    38/-- Truly subquadratic 3SUM: Theorem 22 3SUM. -/
    39axiom algorithm : Theorem_22_3SUM
    40
    41end Lax350013.ThreeSUM
    42
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…