Lax Lean Archive

Version history

Submission versions

  1. lax-228581current versionviewing

    Twin-width can be exponential in treewidth

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

    Twin-Width Can Be Exponential in Treewidth

    Created Lean v4.30.0mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f
    GitHub sourceOpen version

Twin-width can be exponential in treewidth

lax-228581·formalized by Édouard Bonnet @EdouardBonnet · Jan Dreier · Claude Fable 5 (Anthropic) · Codex (OpenAI)·registered·created ·GitHub @1e200ff·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

    For every natural number kk, there is a finite simple graph GG whose treewidth tw(G)\mathrm{tw}(G) and twin-width tww(G)\mathrm{tww}(G) satisfy

    tw(G)≤2k+4and2k<tww(G).\mathrm{tw}(G) \le 2k + 4 \qquad\text{and}\qquad 2^k < \mathrm{tww}(G).
    View annotated paper

    11 pages · 7 marked passages

    Concepts

    Concept map
    3 concepts; 6 descendants hidden
    100%
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimClaim from this 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-228581,
  author = {Édouard Bonnet and Jan Dreier and Claude Fable 5 (Anthropic) and Codex (OpenAI)},
  title = {Twin-width can be exponential in treewidth},
  year = {2026},
  howpublished = {Lax Archive, lax-228581},
  url = {https://laxarchive.org/lax-228581/},
}

    References

    1. Édouard Bonnet and Hugues Déprés. Twin-width can be exponential in treewidth. Journal of Combinatorial Theory, Series B 161:1–14, 2023. doi:10.1016/j.jctb.2023.01.003

    Discussion

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

    Loading discussion…