Back to Problems

HadwigerNelsonAtLeastFive

Specification

Aubrey de Grey improved the lower bound for the chromatic number of the plane to 5 in 2018 using a graph that has >1000 nodes. "The chromatic number of the plane is at least 5" Aubrey D. N. J. de Grey, 2018 (https://doi.org/10.48550/arXiv.1804.02385)

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem HadwigerNelsonAtLeastFive :
    5 ≤ χ(ℝ²)
ID: ErdosProblems__508__HadwigerNelsonAtLeastFive
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.