Four Color Theorem

Stream: mathlib4

[Devon Andrews]

I was wondering if there is any ongoing effort for porting the Coq proof of the Four Color Theorem to Lean. I can always browse Mathlib for everything that has been completed up to this point, but how can I read up on theorems that are actively being worked on?

[Yury G. Kudryashov]

AFAIK, nobody is working on porting the Four Color Theorem proof.

[Yury G. Kudryashov]

I didn't read the original proof but I bet quite a few things should be done differently in Lean/Mathlib because of different design choices made by the library.

[Mario Carneiro]

What is the status of planar graphs in mathlib? Some of the techniques of planar hypermaps from the four color theorem might be useful in mathlib

[Yury G. Kudryashov]

AFAIK, we don't have planar graphs in mathlib yet.

[Yury G. Kudryashov]

Don't we need Jordan curve theorem to talk about planar graphs?

[Yury G. Kudryashov]

BTW, it would be nice to have https://en.wikipedia.org/wiki/Kuratowski%27s_theorem

[Mario Carneiro]

AFAIR planar hypermaps are basically combinatorial objects, you don't really need analysis to deal with them

[Mario Carneiro]

but you probably want JCT to relate planar graphs to actual embeddings in the plane

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/Definition.20of.20planar.20graphs

[Chris Wong]

I believe the thread Yaël linked is the latest on the topic.

I am working on the five color theorem, though I don't think that will conflict with anything, as my current approach uses minors not planarity.