Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Planar Graph Classes

lax-68·formalized by Clemens Kuske·created 2026-09-03·GitHub @8d743cb·Lean v4.30.0 epoch · mathlib c5ea00351c28

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

    This submission collects clean Lean concepts for twelve familiar planar graph classes: planar, outerplanar, maximal outerplanar, grids and walls, triangles, stars, ladders, Halin graphs, wheels, series-parallel graphs, trees, and paths, together with a relational concept for triangulations of planar graphs.

    The definitions follow the standard descriptions in Reinhard Diestel's Graph Theory (6th edition). Straight-line graph drawings are presented as a separate geometric concept and used as compact certificates of planarity, in accordance with Fáry's theorem. Graph minors, represented by connected branch sets, are likewise isolated as a separate combinatorial concept. The planar concept uses that relation directly to exclude K₅ and K₃,₃; Wagner's theorem records the equivalence for finite graphs.

    Topological minors are presented separately as internally disjoint path models. The proof of Wagner's equivalence factors through Kuratowski's subdivision characterization and the special fact that the K₅ and K₃,₃ minor obstructions agree with their topological-minor obstructions. Each graph-class predicate contains only its defining structure: planarity and superclass consequences are stated separately as theorem cards. Proofs are supplied where the result is an elementary projection or composition in the

    Concepts

    thm✓proven claimthm×open claimdefdefinition

    Concept map

    Proven claimOpen claimDefinitionThis submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    assumptions conclusionProven claimOpen claimThis submissionProof — click to open

    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

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    @misc{lax-68,
  author = {Clemens Kuske},
  title = {Planar Graph Classes},
  year = {2026},
  howpublished = {Lax Archive, lax-68},
  url = {https://laxarchive.org/lax-68/},
  note = {draft},
}

    References

    1. Reinhard Diestel. Graph Theory. Springer 173, 2025.

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…