Simple unproven graph theorems

Stream: mathlib4

[Daan Deckers]

Hello mathlib community!

I am a bachelor student who is currently doing his Bachelor End Project. The project entails contributing to one of the open source lean4 libraries. I noticed that there were a lot of "basic" graph theorems missing, (or I couldn't find them). Such as Eulers formula (V − E + F = 2) and K_5 and K_{3,3} being non-planar. I also believe that it is not proven that every connected graph has a spanning tree. Graphs interest me so I was wondering how I could best contribute to this field in mathlib (if my BEP supervisor agrees of course).
Are there any specific suggestions that are recommended I take a look at/attempt?

[Thomas Waring]

Hi! The theorem on spanning trees (forests) is (I hope) almost there — see #33118. The difficulty with theorems about planarity is formalising what it means for a graph to be planar: there is some discussion here and those people might be able to give you more useful pointers :)

[Thomas Waring]

There was also discussion of some possible first projects in this thread which might help!

[Daan Deckers]

Thank you! I'll look into it :)