Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Codex–Terpstra: The fixed cases r=10 and r=11 of the Erdős–Gyárfás balanced-colouring conjecture
OpenAI Codex, directed by Adam Lee Terpstra, "The fixed cases r=10 and r=11 of the Erdős–Gyárfás balanced-colouring conjecture," preprint and computational artifact, 2026.
Verification. The repository's own clean-room audits report that the replay completed and that, for , 33 independent implementation files were frozen beforehand and all 31 selected post-freeze verifier runs passed, including recomputation from the official Ramsey catalogues; nothing was replayed here.
Overview
OpenAI Codex, directed by Adam Lee Terpstra, The fixed cases r=10 and r=11 of the Erdős–Gyárfás balanced-colouring conjecture, preprint and computational artifact (2026), proves two finite instances of Erdős Problem 617: every edge-colouring of with ten colours has an eleven-vertex set omitting a colour, and every edge-colouring of with eleven colours has a twelve-vertex set omitting a colour. These are computer-assisted proofs (sections “Proposed abstract,” “r=10 evidence,” and “r=11 evidence”), audited by the repository's own replays as recorded above. The supplied text contains no numbered theorems, propositions, lemmas, equations, or printed page numbers, so section headings are the finest available locators.
The common reduction, described in “Mathematical setting,” assumes a counterexample and regards each colour class as a graph. Every such graph then has small independence number, while the remaining colour classes impose additional density caps. One chooses a least colour, takes a minimum-degree vertex in its graph, and packs target-colour cliques in the vertex’s nonneighbourhood. The global problem is thereby reduced to a finite collection of extremal one-colour inequalities. The supplied text does not state these reductions formally or define the notation , so their internal hypotheses cannot be reconstructed beyond the descriptions given.
For , the decisive finite bound is
According to “r=10 evidence,” the clean audit regenerated the critical 81- and 82-edge core families, checked 4,923,214 inherited-density subsets and 4,987,794 row-cover partitions, classified the degree-eleven boundary, and replayed all 48 outer comparisons. The terminal comparison is strict by one edge. The audit also detected an unsupported promotion of a whole-row order-51 result to a local constant; the clean recurrence eliminates that constant without changing any recurrence value or margin. Eight rooted 82-edge profiles reduce to four graph-isomorphism orbits, so the discrepancy is reported as overcounting rather than omission. The resulting dependency graph has 35,649 nodes and 90,684 edges, is acyclic, and has every node reachable from the claimed theorem.
For , “r=11 evidence” reports 63 outer comparisons. The sole deficient inherited comparison is , where the available edge budget is 286, whereas the abstract inherited extremal value at order 45 is only
A contextual incidence argument, valid inside an actual putative eleven-colouring but not asserted as an abstract one-colour bound, raises the relevant order-45 floor to 287. This exceeds the budget by one edge, forces seven disjoint target-colour 's, and leads to exclusion of all four stated maximal-packing cases . The independent reconstruction reproduced, among other terminal data, the repaired charge-30 registry (2,111 raw states, 187 canonical states, and 29,208 labelled states), the five two-exception component profiles used in the 76-edge theorem, and 132 marked one-exception states across 15 profiles. It verifies complete coverage of charges , the light-section boundaries, and the distinguished-degree terminals. The supplied text does not state the referenced “76-edge theorem” formally.
The verification protocol is documented in “r=10 evidence,” “r=11 evidence,” and “Trust boundary.” The replay was performed from an acyclic proof graph in a fresh isolated run. For , 33 independent implementation files were frozen before the submitted Python was examined or run; all 31 selected post-freeze verifier runs passed, and the initial and final 401-file manifests agreed. The independent replay confirmed that a 45-state normalization discrepancy, caused by ordered twin endpoints, does not alter any isomorphism class, minimum, or survivor. No proof-assistant formalization or SAT/LRAT certificate is supplied. The explicitly retained trust assumptions include the cited standard extremal theorems, human verification of structural reductions and translations, completeness of fixed-hash McKay catalogues used for , and correct operation of the software and hardware stack (“Trust boundary”).
The scope is deliberately finite: the paper proves only the fixed cases . It neither derives a result for an unbounded family of nor constructs a counterexample. The claim in “Public novelty status” that no earlier public or result was found by 11 August 2026 is a search report, not a mathematical theorem, and expressly does not exclude unpublished or simultaneous work.
Relation to E617
In E617’s notation, let , and for each colour let be the spanning graph on whose edges have colour . A counterexample to E617 would satisfy
because an independent set of size in is exactly an -vertex set whose induced edges omit . Also , so choosing a least colour supplies the initial edge-density constraint used by the paper. Its minimum-degree/nonneighbourhood reduction and clique-packing recurrence then combine this constraint with the simultaneous restrictions from the other colour graphs.
For , the paper substitutes and rules out graphs forming an edge partition of with for every . The usable terminal input is the extremal inequality reported by the source, together with its 48 outer comparisons. Thus it establishes E617 for : some eleven vertices are independent in at least one , equivalently their induced complete graph omits colour .
For , the substitution is . The ordinary inherited order-45 bound does not by itself close the comparison against budget 286. The specifically reusable idea is that one should retain cross-colour incidence information from the original edge partition rather than replace the residual configuration by an arbitrary one-colour graph. In the actual-colouring context this strengthens the relevant floor to 287, after which the clique-packing recurrence forces seven disjoint target-colour 's and excludes . Consequently E617 holds for : some twelve vertices omit a colour.
These arguments contribute two additional positive fixed cases to E617 and suggest a possible strategy for another fixed : derive inherited density bounds, isolate deficient outer comparisons, and repair them using simultaneous-colour constraints before completing a finite packing verification. They do not prove a uniform estimate in , show that the recurrences close for , establish E617 for infinitely many new values, or produce a counterexample. Moreover, because the supplied paper summary does not define or state the structural reductions and terminal results in full theorem form, its numerical bounds should be imported into another argument only through the accompanying replay artifacts and dependency ledgers, with the trust assumptions listed in “Trust boundary.”