Kuratowski's theorem

Stream: Is there code for X?

[Koundinya Vajjha]

Does mathlib know about the Kuratowski criterion for planar graphs? https://en.wikipedia.org/wiki/Kuratowski%27s_theorem
If not, are we anywhere close to proving it? Thanks in advance!

[Yaël Dillies]

mathlib doesn't know about planar graphs :grimacing:
Graph theory is currently at its baby stage. We're having a hard time deciding on the correct definitions.

[Yaël Dillies]

I signed you up to the graph theory stream!