HadwigerNelson Problem Formalization in Lean 4
Description
This repository contains a formalized theorem stating that the plane cannot be colored using 4 colors such that no two points at distance 1 from each other have the same color. Specifically, we verify that the 510vertex graph constructed by Marjin Heule is not 4colorable.
Installation

Install Lean 4 by following the instructions here.

Install CaDiCaL (SAT solver). You can use a different SAT solver capable of producing LRATproofs of unsatisfiability with:
set_option sat.solver <YOUR_SAT_SOLVER_COMMAND>

Run
lake exe cache get
to load the Mathlib cache, then build the project withlake build
. The building process requires more than 20GB of RAM and takes approximately one hour to complete. Alternatively, you can download oleans from Dropbox, put the content to the.lake
directory and only then runlake build
.
Proof Overview
We formalize a standard approach to prove the statement:
 Parse the
.vtx
file containing vertices of the non4colorable unit distance graph.  Find unit distance edges between its vertices and prove that they have exactly unit length using an automatic tactic.
 Reduce the colorability of the finite graph to the satisfiability of some CNF, then use LeanSAT along with an external SAT solver to prove that the graph is non4colorable.
 Reduce the colorability of the plane to the colorability of finite unit distance graphs and complete the proof.
Building Edges
To find edges of the graph, we cast vertex coordinates to Float
and check whether the distance between two given points is close enough to 1. If so, we run the build_edge
tactic that combines norm_num
, ring_nf
, and some extra rewriting of square roots.
Currently, the tactic successfully proves equalities involving numbers that are linear combinations of square roots of naturals over rationals. This is sufficient to build all edges of the 510vertex Heule graph. Unfortunately, the smallest known non4colorable unit distance graph constructed by Jaan Parts is currently beyond the capabilities of build_edge
, as it contains numbers like Sqrt[(5*(7 + Sqrt[33]))/2]
.
TODO
(PRs are welcome)
 Prove that the 509vertex Parts graph is a non4colorable unit distance graph.
 Prove that the plane is 7colorable.
 Construct the non4colorable graph within Lean to make the proof shorter and more independent.
References
 The 510vertex graph by Marjin Heule was obtained from this repository.
 The 509vertex graph by Jaan Parts was sourced from this Polymath thread.