Hardness of coloring three-colorable graphs

Hardness of coloring three-colorable graphs concerns approximate graph coloring: for fixed integers 3 ≤ k ≤ c, it was conjectured to be NP-hard to distinguish k-colorable graphs from graphs that are not c-colorable. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a stronger independent-set form for three-colorable graphs, with a Lean formalization; the constant-palette coloring statement itself had been proved shortly before by Fei, Minzer and Wang, as the manuscript records. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • Khanna, Linial and Safra proved that four-coloring three-colorable graphs is NP-hard, and Guruswami and Khanna gave another proof with bounded-degree variants. The algebraic theory of promise constraint satisfaction of Barto, Bulín, Krokhin and Opršal gave hardness of (2k − 1)-coloring k-colorable graphs, hence five colors for k = 3, and records the conjecture for every fixed 3 ≤ k ≤ c.
  • Guruswami and Sandeep showed that the d-to-1 Games Conjecture with perfect completeness, for any fixed d ≥ 2, implies the constant-palette hardness for three-colorable graphs, using the arc-graph reduction of Krokhin, Opršal, Wrochna and Živný for the final step. Their route gives small independent-set density only under a 2d-colorable promise.
  • Fei, Minzer and Wang proved the 4-to-1 Games Conjecture with perfect completeness, and their Corollary 1.7 gives the three-colorable versus not c-colorable gap for every fixed c. Their Corollary 1.9 gives arbitrarily small independent-set density under an eight-colorable promise. The manuscript cites their report ECCC TR26-179, dated 14 September 2026; the same authors posted arXiv 2610.12378v1 on 8 October 2026.
  • Earlier conditional results already combined three-colorability with small independent-set density: Dinur, Mossel and Regev from their fish-shaped Label Cover conjecture, and Braverman, Khot, Lifshitz and Minzer from the Rich 2-to-1 Games Conjecture. Dinur, Khot, Perkins and Safra, and later Hecht, Minzer and Safra, studied graphs that are three-colorable after deleting a small fraction of vertices.
  • On the algorithmic side, the manuscript cites the bound of O(n^0.19539) colors of Bansal, Huang and Lee, improving Kawarabayashi, Thorup and Yoneda.

The original result

• Claim. Theorem 1.1 of the manuscript states that for every fixed 0 < δ < 1/3 there is a deterministic polynomial-time reduction from 3-CNF formulas to nonempty finite simple graphs such that satisfiable formulas give three-colorable graphs and unsatisfiable formulas give graphs whose largest independent set has fewer than δ times the number of vertices. Corollary 1.2 states that distinguishing k-colorable graphs from graphs that are not c-colorable is NP-hard for every fixed 3 ≤ k ≤ c, which the manuscript describes as recovering the constant-palette theorem. The manuscript describes its new content as the combination of the stronger independent-set soundness with three-colorability of the whole graph, starting from ordinary projection Label Cover.
• Method, as described: layered chains of Label Cover question tuples carry phase vectors on circles, with edges comparing a point with the half-shift of another, so that a satisfying labeling colors the graph with three circle arcs. For soundness, an independent set yields bounded sign-changing Lipschitz functions, which Austin's dimension-independent approximation theorem reduces to boundedly many coordinates. A distributional alignment lemma, proved with finite minimax, Ramsey homogenization and a random-array argument, and a coefficient estimate over finitely many levels then give the density bound. The probability experiment is expanded into unweighted vertices, so the reduction is deterministic.
• Source. The manuscript Hardness of finding large independent sets in three-colorable graphs. Its introduction also mentions two algorithmic preprints posted after its 24 September version, listed below.
• Companion result in the collection. The manuscript cites the collection's Perfect completeness for 2-to-1 games (23 September 2026) as establishing the perfect-completeness premise of Guruswami and Sandeep for d = 2. That manuscript claims Khot's 2-to-1 Games Conjecture with perfect completeness and has its own Lean scope note, lean/docs/105.md. See The 2-to-1 Games Conjecture.
• Formalization, as described by the repository. The scope note lean/docs/106.md states that the formalization gives, for every fixed 0 < δ < 1/3, a deterministic polynomial-time reduction from binary 3SAT to nonempty finite simple graphs with the stated completeness and soundness, and that the complete adjacency-matrix output is included in the runtime bound. The Comparator statement is IndependentSets.lean.
• Catalogue status. The Justin Sun Prize record on GitHub lists the independent-set statement as entry JSP-001056, with status "Solved", Lean proof "reported complete for the stated scope", and eligibility "Pending verification". Its source review of 13 October 2026 states that no clean Lean build, axiom audit, kernel replay or Comparator execution was completed.
• See also The Unique Games Conjecture for the collection's other hardness-of-approximation results.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 18 October 2026)
2026-09-27	I. Narang and Y. Tang, arXiv 2609.33684v1, Improved SDP coloring of 3-colorable graphs from recursive Gaussian certificates	Related work (algorithms)	A randomized polynomial-time algorithm coloring every three-colorable n-vertex graph with O(n(13 − √97)/18 + ε) colors for every fixed ε > 0, about n0.17506, improving the bound of Bansal, Huang and Lee. It does not cite the OpenAI manuscript.	arXiv preprint, version 1.
2026-10-01	E. Anand, arXiv 2610.01071v1, Coloring 3-colorable graphs with O(n4/23) colors via a Gaussian-cover recursion	Related work (algorithms)	A randomized polynomial-time algorithm with O(n4/23) colors, about n0.17391, improving the two preceding bounds. It does not cite the OpenAI manuscript; its AI disclosure states that an extended conversation with OpenAI's Astra found that the approach yielded an improvement.	arXiv preprint, version 1.
2026-10-08	MathVet (GitHub, review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "full": the independent-set gap reduction is stated for every 0 < δ < 1/3, and the coloring corollary is not stated separately, being a one-line consequence. It notes that the reduction is constrained only on encoded formulas and that the proof uses opaque parameter constants, which it calls sound. It records a sandboxed Comparator pass.	MathVet states that its ratings concern whether the Lean states the headline claims.
2026-10-10	cert-machine, openai/math lane K, runs 38040214623 and 38060237164	Verification (kernel replay)	Records that Lean's default kernel accepts the IndependentSets solution, while the nanoda kernel aborted with a stack overflow. The project's notes for the nanoda developers list this challenge among exports that overflow nanoda's fixed 16 MiB worker stack.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list IndependentSets, so this challenge was accepted by con-leche and by Lean's official kernel.	Development journal.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.