Lax Lean Archive

Version history

Submission versions

  1. lax-323828current versionviewing

    Håstad’s inapproximability of Max Clique

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

    Håstad’s inapproximability of Max Clique

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version

Håstad’s inapproximability of Max Clique

lax-323828·formalized by Édouard Bonnet @EdouardBonnet · Codex 6·registered·created ·GitHub @6902a04·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

    Håstad proved that, for every fixed ε>0\varepsilon>0, a deterministic polynomial-time n1−εn^{1-\varepsilon}-approximation of Max-Clique would imply NP=ZPP\mathrm{NP}=\mathrm{ZPP} [1]. We formalize this theorem and extend the inapproximability consequence under NP⊈BPP\mathrm{NP}\nsubseteq\mathrm{BPP} to bounded-error randomized algorithms, using NP from lax-434930 and BPP and ZPP from lax-666725.

    Acknowledgments and reused formalizations. This submission builds substantially on Samuel Schlesinger's complexitylib. We gratefully credit Samuel Schlesinger and the upstream contributors, including Bolton Bailey, credited as the author of the imported Dinur gap-theorem module. The PCP foundation, Cook–Levin machinery, and supporting computational results were adapted from that library, not newly formalized for this submission. The port retains the original copyright and Apache-2.0 notices; its sources and adaptations are documented in the provenance record.

    Concepts

    Concept map
    74 concepts
    100%
    Arbitrarily small projection-game soundnesswith polynomial sizePolynomial-time approximation of the cliquenumberClique inapproximability under NP notcontained in BPPCancellation on a small set of distinctbalanced-predicate inputsCounting and concentration of uniformlybalanced predicatesMultiplicative soundness bounds for sampledtestsFourier analysis on a finite Boolean cubeQuantitative soundness at a fixed evaluationpointFinite quantitative soundness of the CNAtest with side conditionsSoundness of the complete nonadaptivelong-code testSoundness amplification for centeredprojection gamesClique number equals the maximum numberof accepting random choicesHåstad's clique inapproximability theoremThe consistency graph of accepting localviewsExtracting prover strategies from decodedsetsDimension-independent bounds for weighteddouble coversThe consistency graph as an approximationinputEven-cover expansion of a Booleanpolynomial momentExponential concentration on finite productspacesSoundness of the finite FAF compositionThe FAF verifier as a finite local-test systemFree bits of the FAF testFrom FAF acceptance to two-prover successThe finite few-amortized-free-bits testUniform finite probability and even-momenttail boundsRepeated squaring of fortified projectiontestsA small Fourier decoding set independent ofside conditionsFourier shifts, odd tables and disagreementindicatorsAveraging outside a set of coordinatesSampling finite choices with a fixed supply offair bitsThe complete finite game-to-cliqueconstructionA fixed-alphabet regular gap reduction for3-SATNumbering finite graphs and the size of theirencodingFinite graphs and their binary encodingSecond moment and tail bound for thehigh-degree CNA termCancellation outside double covers in highermomentsDimension-independent moments oflow-degree Boolean polynomialsDeterministic bound for the large-coefficientCNA termAccepting local views of a proofLong codes and the complete nonadaptivetestPerfect completeness and local decoding ofthe long-code testFree bits of the complete nonadaptive testIndependent majority repetition reducesbounded errorAgreement among many decoded tablesMixed moments of independently sampledbalanced predicatesNormalizing a long-code table to an oddtableMixed moments of balanced predicates onindependent coordinatesEncoding finite projection-game answers asbinary wordsProjection games from regular constraintsystemsLower concentration of the fibers of auniform random mapBounded-error randomized approximation ofthe clique numberHåstad inapproximability for bounded-errorrandomized algorithmsRandomized computations as NP certificatesThe finite randomized PCP-to-clique transferPolynomial size and approximation gap aftersamplingThe averaged table preserves the answers ofan accepting side-condition testHigher-moment bound for thesmall-coefficient CNA termThe size of the decoding set from largecoefficientsSmall-union weighted double-cover estimateSmall-value projection games for everyregistered NP languageA polynomial-size 3-SAT reduction toarbitrarily small projection-game valueRepetition of local proof testsRandom sparsification of a consistency graphDimension-independent bounds for tupleaveragingFortification by uniformly sampled tuplesA tuple sampler with alphabet-independentmixingBinary encoding of an input and a certificateThe complexity class NPThe complexity class PThe complexity classes RP and coRPPolynomial-time probabilistic TuringmachinesThe complexity class BPPZPP is contained in BPPThe complexity class ZPP
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    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 A

    Cite this

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

    @misc{lax-323828,
  author = {Édouard Bonnet and Codex 6},
  title = {Håstad’s inapproximability of Max Clique},
  year = {2026},
  howpublished = {Lax Archive, lax-323828},
  url = {https://laxarchive.org/lax-323828/},
}

    References

    1. Johan Håstad. Clique is hard to approximate within n1−εn^{1-\varepsilon}. Acta Mathematica 182(1):105–142, 1999. doi:10.1007/BF02392825

    Discussion

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

    Loading discussion…