Planar graphs are surprisingly difficult to formalize. The textbook definition (can be drawn on a plane) is easy to understand, but in code that explodes into a mess of coordinate geometry.
Georges Gonthier, in his proof of the four-color theorem, used a structure called combinatorial hypermaps to encode planar graphs. This approach seems most promising. Before proposing that to mathlib, it would be nice to check that it's suitable for all planar graph theorems, not just four-color.
Resolves YES if mathlib has a definition of planar graph. The code must be on the master branch. Alternative definitions of graphs (like hypermaps) are allowed, as long as there is an embedding from SimpleGraph that preserves planarity.
1,000🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ52 | |
| 2 | Ṁ37 | |
| 3 | Ṁ31 | |
| 4 | Ṁ28 | |
| 5 | Ṁ25 |
People are also trading
Planar graphs are surprisingly difficult to formalize
Isn't it just those graphs that avoids the K_5 and K_3,3 minors?
@levifinkelstein @tfae This is a good point. If there is no separate type, just a proposition isPlanar on SimpleGraph, does this resolve yes?
@levifinkelstein yes, but the forbidden graph characterization is hard to work with, and the maintainers might reject that as the definition for that reason.