Lax Lean Archive

Descriptive complexity: a catalog of thirty NP-complete problems

lax-799700·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·registered·created ·GitHub @5f34068·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

    A catalog of thirty NP-complete decision problems on finite structures, from the descriptive-complexity library, built on the NP core registered as lax-904597: the twenty-one problems of Karp (SAT itself being the core's), the satisfiability variants the reductions run on (not-all-equal SAT and its width-three form, 1-in-SAT), and classical companions: Independent Set, Dominating Set, Subgraph Isomorphism, Set Splitting, the edge-weighted Steiner tree, 3-colorability and kk-colorability for every k≥3k \geq 3. Each problem is a concept: its vocabulary, its defining property, the decision problem it gives, and three claims, that the property is isomorphism-invariant, that the problem's yes-instances are exactly the structures satisfying the property, and that the problem is NP-complete in the core's sense, with NP the class of problems definable in existential second-order logic and hardness by first-order reductions.

    The proofs assume the statements of the core they rest on, Cook–Levin and the closure laws of NP, and nothing else: membership is an existential second-order definition or a first-order reduction to a problem already in NP, and hardness is a first-order reduction, plain, ordered or relativized, from a problem already known hard. The archive's proof network is therefore the reduction tree of the catalog, one edge per reduction, with SAT at its root.

    Thresholds are carried by the instances in unary, as the cardinality of a marked set, so that no order is needed to state a problem; the four problems of Karp's list that are polynomial under that encoding (Knapsack, Partition, 0-1 integer programming, job sequencing) are written in binary, with a linear order on bit positions folded into their yes-instances.

    The proofs are those of version 1.2.2 of the library, sliced to what these statements use; the library and its documentation are at https://github.com/PierreSenellart/descriptive-complexity and https://pierresenellart.github.io/descriptive-complexity/DescriptiveComplexity.html. The Lean code was written with the assistance of several Claude models; the design and the statements are the author's.

    Concepts

    Concept map
    28 concepts; 6 descendants hidden
    100%
    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-799700,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: a catalog of thirty NP-complete problems},
  year = {2026},
  howpublished = {Lax Archive, lax-799700},
  url = {https://laxarchive.org/lax-799700/},
}

    References

    1. Pierre Senellart and Anton Gnatenko. Descriptive Complexity in Lean: Completeness by First-Order Reductions. 2026. arXiv:2609.18261
    2. Pierre Senellart. DescriptiveComplexity: Completeness by First-Order Reductions in Lean. 2026. doi:10.5281/zenodo.21678423 · github.com/PierreSenellart/descriptive-complexity

    Discussion

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

    Loading discussion…