Oct 6, 2026
Lean formalization in OpenAI math repository (Result 106)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Hardness of finding large independent sets in three-colorable graphs'. We prove that, for every fixed 0\lt \delta\lt 1/3, it is NP-hard to distinguish three-colorable graphs from graphs in which every independent set has fewer than δ times the number of vertices. Consequently, for every fixed integer c ≥ 3, finding a proper c-coloring of a three-colorable graph is NP-hard.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 106). The Lean development was not rebuilt locally.