z(20) = 6: resolving the first open case of Erdős problem 758

Summary

Take any network of 20 points, where each pair is either connected or not. Now sort the points into groups so that within each group, either everyone is connected to everyone else (a clique) or nobody is connected to anybody (an independent set). How many groups might you need, in the worst case?

Mathematicians call the answer for $n$-vertex graphs $z(n)$, and Paul Erdős and John Gimbel asked for its values decades ago. The answer was known for every size up to 19 vertices. At 20 vertices, it was known only that the answer is 6 or 7. This candidate computer-assisted proof claims to settle the first open case: $z(20) = 6$.

The proof has two halves with very different characters. The half showing that 6 groups are sometimes necessary is short enough to check by hand: it uses a famously symmetric network on 17 points, the Paley graph, in which no four points are mutually connected or mutually unconnected. The half showing that 6 groups always suffice is where computers earn their keep: every conceivable counterexample is funnelled, through a classical result of Ramsey theory, into two giant logical formulas, and each formula is proved impossible to satisfy — with certificates that four separate programs, one of them formally verified, have each confirmed.

Summary for specialists

The cochromatic number $z(G)$ is the least number of colour classes partitioning $V(G)$ so that each class induces a clique or an independent set, and $z(n) = \max_{|V(G)|=n} z(G)$. Values are known for $n \leq 19$; erdosproblems.com lists $z(20) \in \{6, 7\}$ as the first open case. This release claims $z(20) = 6$.

The lower bound is hand-verifiable: the Paley graph on 17 vertices has no homogeneous 4-set, so $z(\mathrm{Paley}(17)) \geq \lceil 17/3 \rceil = 6$. For the upper bound, since $R(4,4) = 18$, any hypothetical 20-vertex graph needing 7 classes is reduced to configurations built around the two non-isomorphic 16-vertex $(4,4)$-Ramsey graphs. The remaining cross-edge case analysis is encoded as two CNF formulas of 64 variables and 104,524 clauses each, and their unsatisfiability is certified with DRUP and LRAT proof objects, checked by a custom Python RUP checker, a C RUP checker, drat-trim, and the formally verified cake_lpr.

The release also recomputes $R(4,4) = 18$, regenerates the $(4,4)$-Ramsey catalogue, and recomputes the known bounds $z(8) \leq 3$ and $z(12) \leq 4$; the upper bound uses $z(12) \leq 4$ directly. A companion release derives $\mathrm{VR}_2(K_4) = 20$ by reusing the same proof objects.

Technical summary

The upper bound proceeds in three stages. First, since $R(4,4) = 18$, a 20-vertex graph with no two disjoint homogeneous 4-sets contains one homogeneous 4-set, and the other 16 vertices must then form one of the two $(4,4)$-Ramsey graphs on 16 vertices, whose catalogue the release regenerates from scratch. Second, the surviving configurations — cross-edges between the 16-vertex core and the remaining four vertices, together with the demand that the graph have no two vertex-disjoint homogeneous 4-sets — are encoded as two propositional formulas of 64 variables and 104,524 clauses. Third, both formulas are refuted: the DRUP certificates are produced by the solver, translated to LRAT, and accepted by four independent checkers with different trust bases (two hand-written RUP checkers in Python and C, the standard tool drat-trim, and cake_lpr, whose correctness is itself machine-checked down to machine code through the CakeML pipeline).

The lower bound is independent of all of this: Paley(17) is self-complementary and has clique number and independence number 3, so any cocolouring needs at least $\lceil 17/3 \rceil = 6$ classes. The two halves meet at exactly 6.

The SAT layer is certified, including by a formally verified checker. Three computational steps are not formally verified: the program that writes the CNFs (whose correctness is proved on paper in Proposition 5.2 and spot-tested), the C/nauty generation of the Ramsey-graph catalogue, and the C enumeration behind $z(8) \leq 3$ and $z(12) \leq 4$. The rest of the argument is conventional, human-readable mathematics in the 13-page paper.

Evidence, assurance and limitations

Status. An unrefereed, AI-generated candidate computer-assisted proof. A fresh replay was completed on one macOS/arm64 machine on 26 July 2026. No human mathematician has verified the complete argument, and no independent external reproduction, peer review or end-to-end proof-assistant formalisation is claimed.

What was recomputed rather than cited. The finite inputs were regenerated locally from their definitions during that one-machine replay:

The generator reproduces the published $(4,4,n)$ sequence in full; its count of 2 at $n=16$ matches McKay's r44_16.g6 file character for character. Negative controls (cross-core proof/CNF pairings, truncated proofs, injected clauses) were correctly rejected, and drat-trim reports 0 RAT lemmas, so the certificates lie in the RUP fragment.

Where the assurance stops. The proof checkers certify the two exact CNFs, that is, the SAT layer. The graph-to-CNF equivalence, the catalogue generator, the cocolourability program, the mathematical reduction and the software environment remain separate parts of the trusted computing base. The encoding lemmas (that the CNFs mean what they are said to mean) are validated by semantic spot-testing, not proved. Regenerating every input and passing independent checkers is strong validation of the software, not a proof that it is correct: a correlated implementation error in the generator, the translation or the cocolourability checker remains logically possible. Local replay is not external reproduction.

How to inspect or reproduce the recorded checks

Start with the 13-page paper and AI_INDEX.md, which maps each claim to its evidence, hashes and the shortest verification routes. The lower bound needs no software: the paper's six-class certificate for Paley(17) plus three isolated vertices can be checked by hand. From the repository at tag candidate-2026-07-26:

(cd certificates && shasum -a 256 -c MANIFEST.sha256)   # sha256sum -c on GNU/Linux
shasum -a 256 -c RELEASE_MANIFEST.sha256
python3 verification/verify_certificate.py              # exits nonzero on any failed check
drat-trim certificates/z20_core0.cnf certificates/z20_core0.drup
cake_lpr  certificates/z20_core0.cnf certificates/core0.lrat

verify_certificate.py separately constructs both CNFs, spot-checks the encoding against direct computation on 20-vertex graphs and RUP-checks the DRUP proofs. The README gives the nauty-based commands for regenerating the Ramsey catalogue and $z(8) \leq 3$, $z(12) \leq 4$. When automating, require the exact success text s VERIFIED UNSAT from cake_lpr, which can print a checking failure while returning process status 0. Please report attempted reproductions, discrepancies or counterexamples through the repository issue tracker.

Who should care, and why

Why this problem is hard

Cochromatic numbers mix the two classic extremes of graph colouring. A single colour class may be either kind of homogeneous set, so lower bounds cannot lean on standard chromatic machinery, and upper bounds must survive every graph on 20 vertices — roughly $10^{57}$ of them, far beyond enumeration. The Ramsey-theoretic reduction is what collapses this astronomical search space into two finite, certifiable questions. That collapse — not raw computing power — is the heart of the argument.

The most valuable next projects

1. Formalise the encoding

Everything downstream of the two CNFs is already checked by a formally verified tool; everything upstream is ordinary prose plus the catalogue and enumeration programs. The single most valuable follow-up is to machine-check the bridge — the reduction from "every 20-vertex graph is 6-cocolourable" to "these two formulas are unsatisfiable". Formalising the reduction and encoding, together with the catalogue and residual enumeration, in Lean or Isabelle would close the identified gaps and make this, to our knowledge, the first fully verified value in the Erdős–Gimbel table beyond hand range.

2. Push to z(21)

The reduction pattern — concentrate obstructions on a Ramsey core, certify the residual search — did not obviously exhaust itself at 20. The size of the residual search grows, but SAT solvers and proof checkers have headroom. A z(21) attempt would also reveal whether the two-core structure at 20 was a lucky accident or the start of a usable general method.

3. Reproduce independently

The release's own caveats identify what is missing: a second team, with fresh code, regenerating the Ramsey catalogue, re-deriving the reduction, re-encoding the CNFs, and re-checking unsatisfiability. Every needed artefact — instances, certificates, checkers, manifests — is public, so this is an afternoon-to-a-week project for a SAT-literate group, and it is the fastest route to moving the claim up the verification ladder.

Specialist audience candidates

The most natural specialist readers include researchers who maintain and extend the Erdős problems catalogue, those who have computed values in the Erdős–Gimbel table (the z(12) computation in particular), the SAT-certificate community around DRUP/LRAT proof checking and verified checkers such as cake_lpr, and Ramsey-catalogue maintainers. This identifies intellectual proximity, not a prediction that any individual will endorse the manuscript.

The strongest pitch to them is:

The first open entry in the Erdős–Gimbel cochromatic table falls to a hand-checkable Paley bound plus two certified unsatisfiability results — and the uncertified steps are explicitly identified.

How the mathematics was produced

The mathematics in this release was generated by AI systems (Nous Hermes, GPT 5.6 Sol, and Claude models), with human problem selection and mediation. The repository states that no step of the final argument rests on a language-model assertion that was not recomputed by a different system. That policy, together with the certificate architecture, is what makes the claim auditable at all — but it is not a substitute for independent human or formal verification, which the release explicitly lacks.

What is in the evidence package

The repository ships the two CNF instances (z20_core0.cnf, z20_core1.cnf) with DRUP and LRAT refutations; a portable replay checker (verification/verify_certificate.py); the regenerated Ramsey catalogues and calibration recomputations; a 13-page human-readable proof PDF; a machine-readable claim index (AI_INDEX.md); and SHA-256 manifests. The Zenodo deposit archives the release with a DOI.

@misc{z20equals62026,
  title        = {z(20) = 6: resolving the first open case of Erdős problem 758},
  author       = {GPT 5.6 Sol and Claude Opus 4.8 / 5},
  year         = {2026},
  doi          = {10.5281/zenodo.21647645},
  url          = {https://doi.org/10.5281/zenodo.21647645},
  version      = {candidate-2026-07-26},
  howpublished = {Zenodo},
  note         = {Unrefereed; internally replayed evidence package. Press page: https://evidencepress.org/releases/z20-equals-6/}
}