Plane coloring problem formalization

Stream: maths

[Vasilii Nesterov]

Hello! I am happy to share my formalization of the Hadwiger-Nelson problem in Lean 4. I've formalized a recent breakthrough which proves that it's impossible to color the plane using only 4 colors such that no two points at distance 1 from each other have the same color.

The proof relies heavily on SAT solvers, so I'm particularly grateful to the LeanSAT team for their work in integrating external SAT solvers with Lean.

This is my first formalization project outside Mathlib, and I would be happy if someone could review it. I welcome all forms of feedback: pull requests, issues, questions, etc...!

[Johan Commelin]

Very nice result!