Excluded minors and structure theorems

Stream: graph theory

[Viliam Vadocz]

Hey,

I would like to practice Lean by formalizing some of the theorems from my Structural Graph Theory lectures. I am not familiar with what exists in mathlib, so I am wondering whether there is anything for working with graph minors, excluded minors, and structure theorems in general.

For example, I would like to prove that a graph is K_4 minor-free if and only if it can be built starting from graphs on <= 3 vertices by applying 0-, 1-, or 2-clique-sums. I saw complete graphs are defined in mathlib (from a quick search), but I did not see anything about graph minors or operations like clique-sums.

[Shreyas Srinivas]

Probably not

[Chris Wong]

I prototyped minor maps (to support the five-color theorem) here. You might find this useful.
https://github.com/leanprover-community/mathlib4/commits/lambda-fairy/minor/

[Chris Wong]

I believe @Kyle Miller had also formalized minors as a pair of upper and lower bounds. I don't remember the details but there should be some code somewhere.

[Peter Nelson]

Nearly anything to do with minors (and certainly this stuff) really belongs at the level of generality of multigraphs (aka graphs), and these aren't in mathlib yet. There are a lot of hairy design concerns.