# Hardness of coloring three-colorable graphs

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Hardness of finding large independent sets in three-colorable graphs](../../preprints/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026.pdf)

## Scope

The formalized result shows hardness of finding large independent sets even under a three-colorability promise. For every fixed $0<\delta<1/3$, a deterministic polynomial-time reduction maps binary 3SAT formulas to nonempty finite simple graphs. Satisfiable formulas produce three-colorable graphs; unsatisfiable formulas produce graphs whose largest independent set has fewer than $\delta$ times the number of vertices. The complete adjacency-matrix output is included in the runtime bound.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Independent-set hardness in three-colorable graphs | [IndependentSets.lean](../ComparatorChallenges/IndependentSets.lean) |