Lax Lean Archive

Version history

Submission versions

  1. lax-614640current versionviewing

    Tight Inapproximability of Max Independent Set in Triangle-Free Graphs

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceShown on this page
  2. lax-47

    Tight Inapproximability of Max Independent Set in Triangle-Free Graphs

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version

Tight Inapproximability of Max Independent Set in Triangle-Free Graphs

lax-614640·formalized by Édouard Bonnet @EdouardBonnet · Codex 5.6 · Codex 6·registered·created ·GitHub @18be630·Lean v4.33.0 epoch · mathlib db584cd6d46c·

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    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 the main inapproximability theorem of Tight Inapproximability of Max Independent Set in Triangle-Free Graphs.

    Concepts

    Concept map
    12 concepts
    100%
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    Lax253009.Amplification1234567Lax253009.BalancedCancellation12Lax253009.BalancedPredicates123Lax253009.BernoulliSampling12Lax253009.BooleanFourier12345Lax253009.CNAPointSoundness12Lax253009.CNASoundness12Lax253009.CenteredProjection12345678910Lax253009.CliqueCorrespondence1234567Lax253009.EncodedReduction12Lax253009.ExponentialBounds123456Lax253009.FAFComposition12Lax253009.FAFLocalTests1234567Lax253009.FAFPatterns12Lax253009.FAFStrategyExtraction12Lax253009.FAFTest12Lax253009.FiniteProbability123456Lax253009.FourierDecoding12Lax253009.FourierIdentities1234Lax253009.FourierProjection123Lax253009.FreshBitSampling12345Lax253009.GraphEncoding12Lax253009.HighDegreeSoundness12Lax253009.HigherMoments1234Lax253009.Hypercontractivity12345Lax253009.LongCodeCorrectness1234Lax253009.LongCodePatterns12Lax253009.MajorityAmplification12Lax253009.ManyTableConsistency12Lax253009.ProductMoments123Lax253009.ProjectionEncoding123Lax253009.ProjectionGames12Lax253009.RandomFibers12Lax253009.RandomizedReduction123Lax253009.SamplingParameters123Lax253009.SmallCoefficientSoundness12Lax253009.TestRepetition12345Lax253009.TestSampling123Lax253009.TupleAveraging12Lax253009.TupleFortification12345Lax253009.TupleSampler123Lax253009.CNAQuantitativeSoundnessLax253009.DecodedStrategiesLax253009.DoubleCoverBoundsLax253009.FortifiedSquaringLax253009.LargeCoefficientSoundnessLax253009.MixedPredicateMomentsLax253009.SideConditionAveragingLax253009.SmallSupportLax253009.SmallUnionDoubleCoversIndependentSetGapHardnessTriangleFreeIndependentSetHardnessLax759944.TuringRamPolytimeEquivalence
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-614640,
  author = {Édouard Bonnet and Codex 5.6 and Codex 6},
  title = {Tight Inapproximability of Max Independent Set in Triangle-Free Graphs},
  year = {2026},
  howpublished = {Lax Archive, lax-614640},
  url = {https://laxarchive.org/lax-614640/},
}

    References

    1. Édouard Bonnet. Tight Inapproximability of Max Independent Set in Triangle-Free Graphs. 2026.
    2. Johan Håstad. Clique is hard to approximate within n1−εn^{1-\varepsilon}. In 37th Annual Symposium on Foundations of Computer Science 627–636, 1996. doi:10.1109/SFCS.1996.548522

    Discussion

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

    Loading discussion…