Lax Lean Archive

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

Tight inapproximability of Max Independent Set in triangle-free graphs

Lax47.TriangleFreeIndependentSetHardness · concepts/Lax47/TriangleFreeIndependentSetHardness.lean · lax-47

open

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

    Unless NP⊆BPPNP\subseteq BPP, for every constant ε>0\varepsilon>0, Max Independent Set on NN-vertex triangle-free graphs admits no polynomial-time N1/2−εN^{1/2-\varepsilon}-approximation algorithm.

    This is Theorem 1.2. Its proof uses Håstad's general-graph promise-gap hardness theorem and a randomized triangle-removal reduction.

    Concept map
    10 concepts
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax47.Complexity
    2import Lax434930.NondeterministicPolynomialTime
    3import Lax666725.RandomizedPolynomialTime
    4
    5/-!
    6---
    7title: Tight inapproximability of Max Independent Set in triangle-free graphs
    8type: theorem
    9---
    10Unless NP⊆BPPNP\subseteq BPP, for every constant ε>0\varepsilon>0, Max
    11Independent Set on NN-vertex triangle-free graphs admits no polynomial-time
    12N1/2−εN^{1/2-\varepsilon}-approximation algorithm.
    13
    14This is Theorem 1.2. Its proof uses Håstad's general-graph promise-gap
    15hardness theorem and a randomized triangle-removal reduction.
    16-/
    17
    18set_option autoImplicit false
    19
    20namespace Lax47.TriangleFreeIndependentSetHardness
    21
    22open Lax47.Complexity
    23open Lax434930.NondeterministicPolynomialTime
    24open Lax666725.RandomizedPolynomialTime
    25
    26/-- Unless NP⊆BPPNP\subseteq BPP, no polynomial-time N1/2−εN^{1/2-\varepsilon}
    27approximation exists for Max Independent Set on triangle-free graphs. -/
    28axiom not_approximable :
    29 ¬ NP ⊆ BPP →
    30 ∀ (ε : ℝ), 0 < ε → ¬ TriangleFreeMISApproximable ε
    31
    32end Lax47.TriangleFreeIndependentSetHardness
    33
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…