The Borodin-Kostochka Conjecture

The Borodin-Kostochka Conjecture

OpenAI's claim

Correspondence coloring with a forbidden clique: For each fixed $r\ge4$, the paper claims correspondence chromatic number $O_r(\Delta/\log\Delta)$ in graphs with no $K_r$ subgraph and large maximum degree. Ordinary and list-coloring versions follow, and fixed forbidden subgraphs are also covered.

Mathematical statement of the claimed result

Mathematical claim 1.

For every fixed integer $r\ge4$ there are $C_r>0,\Delta_r\ge3$ with the following implication for a finite simple undirected graph $G$, writing $\Delta=\Delta(G)$: if $\Delta\ge\Delta_r$ and no $K_r$ occurs, then \[\chi_{\mathrm{DP}}(G)\le\left\lceil C_r\frac\Delta{\log\Delta}\right\rceil.\] The DP, or correspondence, chromatic number permits a matching of forbidden color pairs across each edge rather than identical color names. The stated corollary replaces $K_r$-freeness by noninduced $F$-freeness for any fixed finite graph $F$, with constants depending on $F$. It does not prescribe the optimal leading constant or strong edge-coloring bounds.

Outline of the argument

Correspondence coloring with a forbidden clique: Random partial-coloring rounds act directly on the graph of available list entries and forbidden matching pairs. Weights track total list supply, individual probabilities, and conflicting edge mass. An entropy-and-mass potential pays for losses when neighboring vertices are colored, including local adjustments for triangles, until the residual lists can be completed.

Formal verification

Family 184 describes Lean coverage for a large independent set in a fixed-clique-free graph at the logarithmically improved scale; correspondence coloring is separate.

Correspondence coloring with a forbidden clique: No manuscript-specific Comparator is listed in the pinned inventory.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, Correspondence coloring graphs with a forbidden clique, 2026-10-05; citation key OAI:Correspondence-Coloring-Graphs-with-a-Forbidden-Clique-October-5-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: cor:forbidden.
• Family 184: Lean scope.
• OpenAI catalogue entry.

The Borodin-Kostochka Conjecture

Definitions and mathematical statement

Let $G=(V,E)$ be a finite simple undirected graph. The degree of a vertex is its number of neighbours, and $\Delta(G)$ is the largest degree. A clique is a vertex subset in which every pair is adjacent; its maximum possible cardinality is $\omega(G)$. A proper vertex colouring is a map $c:V\to\{1,\ldots,q\}$ assigning different colours to adjacent vertices, and $\chi(G)$ is the least such $q$.

The Borodin--Kostochka conjecture states that for every $G$ satisfying $\Delta(G)\ge9$, \[ \chi(G)\le\max\{\Delta(G)-1,\omega(G)\}. \] In particular, if $G$ has no clique of size $\Delta(G)$, the conclusion requires a proper colouring with at most $\Delta(G)-1$ colours. If a large clique is present, the formula explicitly retains the unavoidable clique lower bound.

The degree threshold is part of the assertion: no claim is made here for graphs with maximum degree eight or smaller. The condition is on maximum degree, not minimum degree or average degree. The graph need not be connected, regular, planar, or from a particular forbidden-subgraph class. Ordinary colour palettes are used; requiring a colouring from prescribed lists at the vertices would be a stronger conjecture.

The target is an existence theorem uniformly over graph size. It does not merely ask for an estimate that approaches $\Delta(G)$ asymptotically: the saving of one full colour whenever the clique bound permits it is the exact conclusion.

Short English statement

Does every graph of maximum degree at least nine need at most the larger of its clique number and one less than its maximum degree colours?

Research attempt

Scope and process.

GPT-6 Astra Ultra, 1 October 2026. This attempt keeps the catalogue statement above, checks primary literature, and develops a restricted argument with an adversarial gap audit. The proofs below are the mathematical output of this attempt, not a claim of novelty or external certification.

Literature and attack plan.

Dvořák, Kang and Mikšaník [R1] prove a correspondence-colouring version for maximum-degree bounds at least $3\cdot10^9$, strengthening earlier large-degree results. The threshold in the catalogue is nine, so that result does not by itself settle the statement here. We develop a self-contained reduction for the difficult clique-free case and an exact proof for graphs supplied with a perfect elimination ordering. Kempe-chain obstructions identify the point where a greedy extension ceases to be justified.

Reducing a putative obstruction.

Fix $D\ge9$ and suppose $\Delta(G)\le D$, $\omega(G)\le D-1$, but $G$ is not $(D-1)$-colourable. Choose an induced subgraph $H$ of minimum order with the latter property and put $q=D-1$. Every $H-v$ has a $q$-colouring. If $d_H(v)\le q-1$, at most $q-1$ colours occur on its neighbours, so a missing colour extends that colouring to $v$, a contradiction. Therefore \[ D-1\le\delta(H)\le\Delta(H)\le D. \tag{1} \] Moreover, $H$ is connected: otherwise every component, being a proper induced subgraph, could be coloured separately with the same palette.

The reduction also proves a useful subclass result without any structural theorem: if every nonempty induced subgraph of $G$ has a vertex of degree at most $D-2$, repeated removal and reverse greedy colouring give $\chi(G)\le D-1$. Any counterexample to this part of the conjecture must instead contain the high-degree core $1$.

The local Kempe constraint.

Suppose $v\in V(H)$ has degree exactly $q$, and fix a $q$-colouring of $H-v$. Every colour must appear on $N_H(v)$; with exactly $q$ neighbours, each appears exactly once. Write $u_i$ for the neighbour coloured $i$.

For any two different colours $i,j$, the vertices $u_i,u_j$ must belong to the same connected component of the subgraph induced by colours $i,j$. Otherwise interchange $i,j$ in the component containing $u_i$. This preserves properness: edges within that component remain bichromatic, edges to other colours remain proper, and an edge to an $i$- or $j$-coloured vertex outside the component would contradict the definition of component. After swapping, no neighbour of $v$ has colour $i$, because its unique such neighbour changed to $j$ while $u_j$ was not changed. Assigning $i$ to $v$ gives the forbidden $q$-colouring of $H$.

Hence every pair of the uniquely coloured neighbours is joined by a corresponding two-colour path. This is a necessary condition, not a statement that the neighbours form a clique. A two-colour path can have many internal vertices, so replacing "same component" by "adjacent" would be the first unjustified leap in this strategy.

A complete proof for elimination-ordered graphs.

Suppose $G$ has an ordering $v_1,\ldots,v_n$ such that the later neighbours of each $v_i$ form a clique. Colour in reverse order. When reaching $v_i$, its already coloured neighbours number at most $\omega(G)-1$, since together with $v_i$ they form a clique. A palette of $\omega(G)$ therefore always has a free colour. This proves \[ \chi(G)=\omega(G) \] for every graph with such an ordering, and hence proves the catalogue inequality on this subclass for every maximum degree, in particular $\Delta\ge9$. The proof requires the stated ordering; it does not assert that arbitrary graphs admit it. Complete graphs, trees rooted and removed from leaves, and recursively clique-attached examples provide immediate verifiable instances.

Verification.

The minimality argument does not assume the induced subgraph $H$ still has maximum degree at least nine; it works with the fixed ambient bound $D$ throughout. This avoids incorrectly applying the conjecture recursively to lower-degree subgraphs. The Kempe argument at a degree-$q$ vertex uses uniqueness of each neighbour colour. At a degree-$q+1$ vertex a colour may repeat, so the same swap need not free any colour; that case is not covered. Finally the clique restriction $\omega\le D-1$ was stated explicitly, and no reduction of the entire conjecture to this restricted case is claimed without additional results.

First gap and final status.

The attempt proves the elimination-order case, the low-degeneracy case, and necessary degree/Kempe constraints on an obstruction in the difficult clique-free regime. It does not exclude cores with degrees $D-1,D$, or convert the two-colour connecting paths into the forbidden clique. The full Borodin--Kostochka conjecture is UNRESOLVED by this attempt.

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, supplied problems.json, record 3122 (OPG-37670), OpenGarden collection. Catalogue identity and source transcription; CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Open Problem Garden, The Borodin-Kostochka Conjecture. Original problem and discussion; the mathematical formulation below is expanded from the supplied source record. http://www.openproblemgarden.org/op/the_borodin_kostochka_conjecture.
• R1 Z. Dvořák, R. J. Kang and D. Mikšaník, On Borodin--Kostochka conjecture for correspondence coloring, arXiv:2603.14427 $2026$. Primary abstract checked for its explicit large-degree threshold. https://arxiv.org/abs/2603.14427.