Graph minors and structure theorems

Stream: Is there code for X?

[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 simple graphs and complete graphs are defined in mathlib (from a quick search), but I did not see anything about graph minors or operations like clique-sums. Are these things in mathlib?

(This is a repost from #graph-theory for visibility)