R(12,12) ≥ 1661 by extending the Mathon–Shearer coloring

Introduction

The Ramsey number $R(k,s)$ is the least $N$ such that every red/blue coloring of the edges of $K_N$ contains a red $K_k$ or a blue $K_s$. A coloring of the edges of $K_n$ with no red $K_k$ and no blue $K_s$ is called a $(k,s)$-coloring and shows that $R(k,s) > n$. Lower bounds for small Ramsey numbers are proved in this way, by constructing colorings; Radziszowski’s survey [11] collects the known bounds.

For $R(12,12)$ the lower bound has improved in small steps. Mathon [7] and Shearer [12] constructed an $(11,11)$-coloring on 1596 vertices, which shows that $R(11,11) \ge1597$. Xu, Shao and Radziszowski [16] proved that $R(k,s+1) \ge R(k,s) + 2k - 2$ for $k \ge5$ and $s \ge2$; applying the inequality twice, with the two colors interchanged in between, gives $R(12,12) \ge1639$ [11]. In 2017, Tatarevic found a $(12,12)$-coloring on 1639 vertices by a computer-assisted construction, so that $R(12,12) \ge1640$ [13]. Tatarevic recently proved that $R(k+1,s+1) \ge R(k,s) + 2k + 2s$ for $5 \le k \le s$ [14], by a construction that adds $2k + 2s$ vertices to a $(k,s)$-coloring. Applied to the Mathon–Shearer coloring, the construction gives $R(12,12) \ge1641$.

The coloring is built from the Mathon–Shearer coloring. We delete 21 of its 1596 vertices, namely a red $K_{10}$, a blue $K_{10}$ and one further vertex, and add a set $T$ of 85 vertices. Toward the 1575 remaining vertices, each vertex of $T$ either has the same colors as one of the deleted vertices, and is then called a copy of that vertex, or has a single color; the colors inside $T$ were found by a computer search. In these terms, Tatarevic’s construction [14] deletes a red $K_{10}$ and a blue $K_{10}$ and adds a set $T$ of 64 vertices: the 20 deleted ones and 44 new ones, each a copy of a deleted vertex or of a single color. A monochromatic clique splits into a part in $T$ and a part among the remaining vertices, and the second part has at most 10 − $\omega$ vertices, where $\omega$ is the size of the largest clique of the same color that the Mathon–Shearer coloring has among the deleted vertices copied by the first part. So it suffices to check a finite condition on $T$ (Theorem 3.3); in general, a monochromatic clique of $T$ may have at most $1+\omega$ vertices, so deleting a red and a blue $K_{10}$ leaves room for large cliques of both colors in $T$.

The key to the construction, and its new ingredient compared with earlier colorings of this shape, is a symmetry of the Mathon–Shearer coloring: every vertex $v$ has an antipode $\bar{v}$, whose color to every other vertex is the opposite of the color of $v$ (Lemma 2.2). Suppose that a monochromatic clique contains a copy of $v$ and a copy of $\bar{v}$. A remaining vertex in this clique would have the color of the clique to both copies, hence to both $v$ and $\bar{v}$, which is impossible. So the clique lies inside $T$, and for such cliques the finite condition only requires that $T$ contain no monochromatic $K_{12}$. For two deleted vertices that are not antipodal, in contrast, the condition allows at most 8 vertices of $T$ that copy either of them (Proposition 5.1). Together, the red and the blue $K_{10}$ contain one antipodal pair; the further deleted vertex is the antipode of a vertex of the blue $K_{10}$, which creates a second pair.

Our earlier colorings on 1641 and 1657 vertices [4, 5], released with Lean proofs and computer checks but not described in a paper, have the same shape; their deleted vertices contain only the first antipodal pair, which their proofs do not use. Appendix § 10 describes them, an unreleased coloring on 1650 vertices between them, and how all of these colorings were found.

Apart from the fact that the Mathon–Shearer coloring is an (11, 11)-coloring, which we quote, the proof uses an elementary property of this coloring (Lemma 2.2) and a finite check that takes a computer about two seconds. The result has also been checked by computer in several independent ways (Appendix § 9): two exhaustive searches by separate programs confirm that the coloring has no monochromatic $K_{12}$, and the theorem, including Fact 2.1, is formally verified in Lean 4.

The Mathon–Shearer coloring and its antipodes

Let $q=797$, a prime with $q\equiv1\pmod{4}$, and let $S$ and $N$ be the nonzero squares and the nonsquares of $\mathbb{F}_q$; then $-1\in S$. The coloring $M=M(797)$ has the $2q+2=1596$ vertices $A_x$, $B_x$ ($x\in\mathbb{F}_q$), $a$ and $b$; identifying $\mathbb{F}_q$ with $\{0,\ldots,796\}$, we number them $A_x=x$, $B_x=797+x$, $a=1594$, $b=1595$:

• $A_xA_y$ and $B_xB_y$ are red if and only if $x-y\in S$;

• $A_xB_y$ is red if and only if $x-y\in N$;

• $a$ is red to every $A_x$, $b$ is red to every $B_x$, and all other pairs are blue.

We write $M(u,v)$ for the color of $uv$.

The antipode of a vertex $v$ is $\bar{v}$, where $\overline{A_x}=B_x$, $\overline{B_x}=A_x$, $\bar{a}=b$ and $\bar{b}=a$.

In the terminology of Mathon [7], the red pairs of $M(797)$ form an antipodal distance-regular graph of diameter 3, and $\bar{v}$ is the unique vertex at distance 3 from $v$ in this graph.

Clone extensions and the projection criterion

Throughout, $c$ stands for one of the two colors, red or blue, and $\bar{c}$ for the other one. Two vertices are $c$-adjacent if the pair between them has color $c$, and a $c$-clique is a set of pairwise $c$-adjacent vertices.

For a color $c$ and $D \subseteq\Sigma$, we define the capacity function $\operatorname{cap}_{c}$ by

We call the first case the antipodal rule.

Proof. Let $Q$ be a $c$-clique and $K$, $K^{\circ}$ as in Lemma 3.2. If $K = \varnothing$, then $Q$ is a $c$-clique of $M$ and $|Q| \leq10$. If $K$ contains a constant vertex of color $\bar{c}$, or $D(K)$ contains an antipodal pair, then $K^{\circ} = \varnothing$ and $|Q| = |K| \leq11$ by (i). Otherwise $|Q| = |K| + |K^{\circ}| \leq(1 + \omega_{c}(D(K))) + (10 - \omega_{c}(D(K))) = 11$ by (ii) and Lemma 3.2(c). □

Remark 3.4. Condition (ii) has to be checked for all $c$-cliques of $T$, not only the maximal ones: when $K$ gains a copy of the second vertex of an antipodal pair, its capacity jumps to 11, so $K$ can violate (ii) although its maximal extensions satisfy it. Our check therefore enumerates all cliques. Without the antipodal rule, maximal cliques would suffice, after removing their constant vertices of color $\bar{c}$ (Appendix § 10).

Remark 3.5. Replacing the bound $10 - \omega_{c}(D)$ of Lemma 3.2(c) by the exact value $e_{c}(D)$, the largest number of vertices of $V^{\circ}$ that are pairwise $c$-adjacent in $M$ and $c$-adjacent to every vertex of $D$, and hence $\operatorname{cap}_{c}(D)$ by the exact capacity $11 - e_{c}(D)$, turns Theorem 3.3 into a necessary and sufficient condition, provided all cliques are checked. Since $e_{c}(D) \leq10 - \omega_{c}(D)$, and $e_{c}(D) = 0$ by Lemma 2.2 if $D$ contains an antipodal pair, the exact capacity is at least $\operatorname{cap}_{c}(D)$. The search of Appendix § 10.§ 2 used the exact capacities; the coloring of § 4 satisfies the conditions of Theorem 3.3 as stated, so its proof does not need them.

The coloring

Let $C = \{c_1,\ldots,c_{10}\}$ and $I = \{i_1,\ldots,i_{10}\}$ be the sets of vertices of $M$ in Table 1, given by name and by number (§ 2).

$p$	1	2	3	4	5	6	7	8	9	10
$c_p$	$B_{133}$ 930	$B_{129}$ 926	$B_{776}$ 1573	$B_{541}$ 1338	$B_{682}$ 1479	$B_{686}$ 1483	$B_{695}$ 1492	$B_{785}$ 1582	$B_{789}$ 1586	$b$ 1595
$i_p$	$B_{264}$ 1061	$B_{791}$ 1588	$B_{779}$ 1576	$B_{752}$ 1549	$B_{757}$ 1554	$a$ 1594	$B_{675}$ 1472	$B_{760}$ 1557	$B_{282}$ 1079	$B_{470}$ 1267

The nine labels $x$ of the vertices $B_x$ in $C$ have pairwise differences in $S$, and $b$ is red to every $B_x$, so $C$ is a red $K_{10}$; the nine labels in $I$ have pairwise differences in $N$, and $a$ is blue to every $B_x$, so $I$ is a blue $K_{10}$. Put $\Sigma= C \cup I \cup\{A_{675}\}$. Here the vertex $A_{675}$, with number 675, is the antipode of $i_7 = B_{675}$, with number 1472; we write $\bar{i}_7 = A_{675}$. So $\Sigma$ contains exactly two antipodal pairs: the pair $\{a,b\} = \{i_6,c_{10}\}$ inside $C \cup I$, and the new pair $\{i_{7},\bar{i}_{7}\}$. In all, $|\Sigma| = 21$ and $|V^{\circ}| = 1575$. The 85 vertices of $T$, their types and all colors inside $T$ were found by the computer search of Appendix § 10.§ 2.

The file graph/r1212_1660.graph has 1660 rows of 1660 characters, both numbered from 0; for $v \ne w$, character $w$ of row $v$ is 1 if $vw$ is red and 0 if blue, and the diagonal is 0. Rows 0–1574 are the vertices of $V^{\circ}$ in increasing order, with the colors of $M$. Rows 1575–1659 form $T$; their types are read from the file, and Table 2 gives the number of vertices of each type. The colors inside $T$ are given by the file only; they are not described by a formula.

type	number of vertices
constant red, constant blue	11 each
$i_{7}$	4
$\bar{i}_{7} = A_{675}$	2
each of the other 19 vertices of $C \cup I$	3
total	85

Proof. The script check_antipodal_projection.py verifies that the file is a clone extension with the above $\Sigma$: rows 0–1574 equal $M$ restricted to $V^{\circ}$, rebuilt from the definition, and each of the 85 other rows is, on $V^{\circ}$, constant or equal to the row in $M$ of exactly one $g \in\Sigma$. The script also checks Lemma 2.2 by brute force, that is, it confirms $M(v,w) \ne M(\bar{v},w)$ for each of the 798 antipodal pairs $\{v,\bar{v}\}$ and each of the 1594 other vertices $w$; it then verifies the conditions of Theorem 3.3: the largest red and the largest blue clique inside $T$ have 11 vertices, and condition (ii) holds for all 342,582 red and all 236,100 blue cliques of $T$ without a constant vertex of the other color. The values $\omega_c(D)$ are computed for all $2^{21}$ subsets $D$ of $\Sigma$; for each color, on $\Sigma$ itself and on 200 random subsets, they agree with those computed by the Python graph library networkx. By Theorem 3.3, the coloring has no monochromatic $K_{12}$.

Theorem 1.1 follows. The antipodal rule is needed: with $\operatorname{cap}_c(D) = 1 + \omega_c(D)$ for every $D$, condition (ii) fails for 5,332 cliques (5,123 red, 209 blue). For each of these cliques $K$, the set $D(K)$ contains an antipodal pair: the new pair $\{i_{7},\bar{i}_{7}\}$ for 5,309 of them, and only $\{a,b\}$ for the other 23. Of all cliques $K$ checked, 7,125 red and 10,112 blue ones have an antipodal pair in $D(K)$.

Why an antipodal pair helps

Condition (ii) of Theorem 3.3 with $|D| \le2$ already strongly limits the number of vertices of each type.

Proof. For both colors $\omega_c(\{g\}) = 1$, so $\operatorname{cap}_c(\{g\}) = 2$. The pair $\{g,h\}$ is a clique of $M$ in the color $M(g,h)$ but not in the other color, so $\operatorname{cap}_c(\{g,h\})$ is 3 for $c = M(g,h)$ and 2 for the other color. Use $R(3,3) = 6$ and $R(3,4) = 9$ [11].

In our earlier coloring on 1657 vertices [5], which does not use antipodal pairs, the types $i_1 = B_{264}$ and $c_7 = B_{695}$ have 4 vertices each, so this pair is already at the limit. For $\Sigma= C \cup I$ the exact values $e_c(D)$ of Remark 3.5 agree with $10 - \omega_c(D)$ for $|D| \le3$, except for the sets $D$ containing $\{a,b\}$, for which $e_c(D) = 0$; so they do not relax these constraints. For an antipodal pair, $\operatorname{cap}_c(\{g,\bar{g}\}) = 11$ and Proposition 5.1 gives no joint limit. The present coloring improves on [5] at this point: its types $i_7$ and $\bar{i}_7$ have only $4 + 2 = 6$ vertices, but 5,309 of the cliques that contain copies of both would violate (ii) without the antipodal rule (§ 4). Since every vertex of $M(797)$ has an antipode, any $g \in\Sigma$ whose antipode lies in $V^\circ$ can be given a partner by moving $\bar{g}$ into $\Sigma$; the vertex $\bar{g}$ itself then becomes a copy of $\bar{g}$ in $T$, so the number of vertices does not change. We do not know whether the new pair is necessary for 1660 vertices. With $\Sigma= C \cup I$, our searches found no coloring on more than 1657 vertices (Appendix § 10.§ 3); this is only weak evidence that the new pair is needed. Our attempts to reach 1661 vertices by the same method failed; they are described in Appendix § 10.§ 3.

Data and code availability

The 1660-vertex coloring, the check script, checkers A and B (Appendix § 9), both exhaustive search programs with the outputs of our runs, the controls, and the Lean proof with the records of its checks are available at [6]; Appendix § 9 gives the hash of the coloring and the archived versions. The programs and logs of the searches in Appendix § 10 are not public.

Use of AI

This work was carried out with the AI system Claude (Anthropic, model Claude Opus 5.5), used through the coding agent Claude Code. The system designed and ran the searches and the computer checks, wrote the Lean proof, and drafted this paper. The work continues [5], which started from exploratory work by GPT-6 Astra (OpenAI); its history is described there. The author directed the project and takes responsibility for the paper; the AI system is not an author. The correctness of the result does not rely on the AI system, but on the proof given here, whose formalization is checked by the Lean kernel and by nanoda, and on the exhaustive searches (Appendix § 9).

Acknowledgments

The author thanks Milos Tatarevic for publishing the paper [14] together with the Lean development and programs [15], on which the formal proof builds, and Stanisław Radziszowski for many years of attention to these questions and for collecting the known bounds in [11]; both answered the author’s messages with encouragement. Thanks also go to Gábor Lippert, whose lively and engaging lectures introduced the author to this subject, for positive and encouraging conversations, and to Chris Beasley, the author’s advisor, for guidance and help and for the freedom to pursue this research.

Computer verification

The proof of Theorem 4.1 rests on one finite computation, the check of Theorem 3.3. Table 3 lists this check together with the independent ones. The two exhaustive searches use no structure of the coloring and do not depend on Fact 2.1. The other checks depend on Fact 2.1; they come from three programs, written separately, in different sessions of the AI system: the check script of Theorem 4.1 and two checkers, A and B, of which A runs in two modes. Each program reads the types from the file, or checks the declared types against it. The checks in this appendix ran on an Apple M4 Mac mini. The programs, data and logs of these checks are in the repository [6].

check	method	result
exhaustive search, program of [4] (unchanged)	for each vertex $v$ and color $c$, search the later $c$-neighbors of $v$ for a $c$-clique on 11 vertices	3,320/3,320 tasks “none”; 2.24 $\times10^{11}$ nodes; 15.46 CPU-hours
independent exhaustive search	as above, but with the vertices of each color ranked in a degeneracy order, so the subproblems differ; its own branch and bound	3,320/3,320 tasks “none”; 2.40 $\times10^{11}$ nodes; 17.93 CPU-hours
check_antipodal_projection.py (this paper)	Theorem 3.3, all cliques	PASS; 1.8 s, one thread
checker A, bound mode	Theorem 3.3, all cliques	PASS; clique counts and histograms of $\operatorname{cap}_c(D(K))-|K|$ identical to the script’s
checkers A and B, exact mode	Remark 3.5, all cliques, $e_c$ computed exactly	both PASS

Controls. The following controls test the checks themselves.

• Flipped edge. Flipping the color of the edge between the constant red vertices in rows 1615 and 1616 makes check_antipodal_projection.py report two violated cliques, with $D=\varnothing$ and $D=\{i_7\}$. Checker A in exact mode reports the same two cliques, extends each to an explicit red $K_{12}$ of the modified file, and confirms every edge.

• No antipodal rule. Without the rule, the same script fails with 5,332 violations, as in § 4. Checker A in bound mode, without the rule, reports the same number.

• Structure. Flipping an edge inside $V^\circ$, or between $T$ and $V^\circ$, makes the script stop with an error.

• Search programs. Both exhaustive programs were tested on November 3, 2026, when we reverified [5]: the first reproduced the published run of [5] task by task and found planted $K_{12}$s; the second agreed with an exact oracle on 528 random graphs, caught 4 deliberately broken versions of itself and found all 14 planted $K_{12}$s. Both runs here used those binaries. The records of these tests are not public; both programs and the outputs of both runs are released with the coloring.

Formal proof in Lean. We have formalized Theorem 1.1 in Lean 4 (version 4.32.1) with Mathlib [2, 8]:

theorem RamseyIncrement.R1661.r1212_lower_bound : 1661 ≤ ramseyNumber 12 12

• The statement. ramseyNumber is the definition of [4, 5], from Tatarevic’s Lean development [15]: the least $n$ such that every red/blue coloring of $K_n$ has a red $K_k$ or a blue $K_s$. An audit file restates it in Mathlib’s terms, for a graph on Fin $1660$ and its complement. The coloring is defined on $V^\circ\sqcup\{0,\ldots,84\}$, with tables generated from the graph file.

• The argument follows Theorem 3.3. The proof uses Fact 2.1, proved in Lean in [4]; Lemma 2.2, proved in Lean from $-1 \in S$; the colors of $M$ on $\Sigma$; and finite checks on $T$, which the Lean kernel evaluates. A clique with a constant vertex of the other color, or with copies of both vertices of an antipodal pair, lies inside $T$ by Lemma 3.2, and the kernel checks that $T$ has no monochromatic $K_{12}$. For all other cliques the proof reuses the defect lemma and the four small checks of [5], applied to $T$ with the edges between copies of antipodal types removed. These checks cover every such clique, not only the maximal ones, so Remark 3.4 causes no difficulty. The proof does not use the exhaustive searches.

• Axioms: only propext, Classical.choice and Quot.sound. No sorry, no native_decide.

• Independent kernels. leanchecker replayed each of the 25 modules of the proof separately, and nanoda [9], a Lean kernel written separately in Rust, checked an export of the theorem made with lean4export [3], together with all 29,313 declarations it uses, Mathlib included. Both accepted the proof. As a control, nanoda rejected a copy with one bit of a table changed. Of the 25 modules, 19 come unchanged from [4] and one, the defect lemma, from [5]; 5 are new.

• Not part of the proof: that the coloring defined in Lean is the file. A script rebuilds all $1660^2 = 2{,}755{,}600$ entries from the Lean tables, following the definitions, and they equal the file; so do the 85 rows of $T$ that Lean’s interpreter evaluated.

Data. The coloring is the file graph/r1212_1660.graph in [6], in the format of § 4: 1660 lines of 1660 characters, 2,757,260 bytes. The numbering of the vertices of $M$ in § 2 is the same as in the files of [4, 5]; the rows of the present file are ordered as in § 4. The SHA-256 hash of the file is

07c5cbb696c1d7662870b42e6a1c508e7ef46bf2313f01d297f914e62448867d

Version 1.0.1 of the repository is archived at https://doi.org/10.5281/zenodo.24087657, and https://doi.org/10.5281/zenodo.23963534 refers to all versions. The files of the repository and of [4, 5] number the vertices of $C$ and $I$ from 0: their $c_j$ and $i_j$ are our $c_{j+1}$ and $i_{j+1}$, and the name 16bar in the outputs of the repository stands for $\bar{i}_7$. The repository also lists the type of every vertex of $T$.

How the colorings were found

Table 4 lists our colorings, together with the one given by Tatarevic’s construction. All of them have the shape of § 3: they consist of $V^\circ$ and a typed set $T$, and each vertex of $T$ copies a vertex of $\Sigma$ or has a single color toward $V^\circ$. Except in the last row, $\Sigma= C \cup I$, so that $|V^\circ| = 1576$, and $T$ contains the 20 vertices of $C \cup I$, as copies of themselves with the colors of $M$ among them. This $\Sigma$ already contains the antipodal pair $\{a,b\} = \{i_6,c_{10}\}$, but the proofs of [4, 5] do not use it.

bound	$|V^\circ|$	$|T|$	new ingredient	source
1641	1576	64	Tatarevic’s construction applied to $C$ and $I$	[14]
1642	1576	65	one more vertex after recoloring 7 pairs	[4]
1651	1576	74	colors inside $T$ found by a SAT solver	not released
1658	1576	81	the solver also chooses what each vertex copies	[5]
1661	1575	85	a second antipodal pair; local search	this paper

Tatarevic’s construction, applied to $C$ and $I$, already has this shape: each of its 44 new vertices is a copy or has a single color toward $V^\circ$, so that $|T| = 64$. In [4], recoloring 7 pairs inside $T$ made room for one more vertex, so that $|T|=65$. The release [4] used Theorem 3.3, without the antipodal rule, as one of its checks; the searches below use the criterion to find colorings. None of the searches is part of a proof: every coloring that we report was checked afterwards, the present one as described in Appendix § 9.

Maximal cliques. Without the antipodal rule, that is, with $\operatorname{cap}_c(D)=1+\omega_c(D)$ for all $D$, condition (ii) of Theorem 3.3 only has to be checked for the maximal $c$-cliques of $T$, after removing their constant vertices of color $\bar{c}$. When a vertex is added to a $c$-clique $K\subseteq T$, $|K|$ grows by one and $\omega_c(D(K))$ by at most one, so the slack $1+\omega_c(D(K))-|K|$ cannot increase; a violation of (ii) therefore persists in every larger $c$-clique without a constant vertex of color $\bar{c}$. The checks of [4, 5] and the searches of Appendix § 10.§ 1 rely on this. With the antipodal rule the slack can increase (Remark 3.4): if $K$ contains copies of $g$ but none of $\bar{g}$, adding a copy of $\bar{g}$ raises the capacity to 11.

From 1641 to 1657 vertices

These searches ran on October 29 and 30, 2026, on a Windows computer. They used Theorem 3.3 without the antipodal rule, with $\Sigma=C\cup I$ and the colors among $C\cup I$ fixed; as explained above, it then suffices to check maximal cliques.

The encoding. With the types of the vertices of $T$ fixed, every pair inside $T$ that is not inside $C\cup I$ is a Boolean variable, true if the pair is red. A $c$-clique $K\subseteq T$ violates the criterion if $|K|\ge12$, or if $K$ has no constant vertex of color $\bar{c}$ and $|K|>1+\omega_c(D(K))$; its clause says that some pair of $K$ that is a variable does not have color $c$. There are far too many such cliques to write all clauses down, so the solver started with none. Each solution was checked by enumerating the maximal cliques of $T$; the clauses of all violated cliques were added, and the solver was run again, until a solution passed the check. Every solution that we kept was checked again by a separately written implementation of the criterion and by the check script of [4].

1650 vertices. Starting from the 45 new vertices of [4], with their types, we added one copy at a time. The vertices of $C\cup I$ with the fewest copies were tried first, and the first choice for which the solver found a solution within 60 seconds was kept. Already after the first step, the colors found differ from those of [4] in several hundred pairs. The procedure reached 53 new vertices; a second pass, which started the solver from the previous solution and kept the clauses found so far, added a 54th. The 54 new vertices are 11 constant red, 11 constant blue and 32 copies; the constant vertices are those of [4]. For a 55th vertex, every choice timed out except one, which the solver reported infeasible.

1657 vertices. Next the types of the new vertices became variables as well. For each new vertex, indicator variables say which vertex of $C \cup I$ it copies; at most 4 new vertices copy the same vertex, so that each type has at most 5 vertices, as Proposition 5.1 requires; and the clause of a violated clique also allows that some new vertex of the clique has another type. The constant vertices were already 11 of each color, the most that the criterion allows: since $\operatorname{cap}_{c}(\varnothing) = 1$, the constant vertices of color $c$ span a $\bar{c}$-clique. So all new vertices are copies. With the solver CaDiCaL 1.9.5 [1], called through PySAT [10], each step added one vertex. From 54 to 60 new vertices the steps took between 10 seconds and 18 minutes, and the 61st vertex took 21 minutes. For a 62nd vertex, none of six solver configurations finished within 30 minutes; this is a time limit, not a proof that no such vertex exists. Symmetry-breaking constraints, and clauses for all violated sets of at most 3 vertices added in advance, did not speed up the search.

From 1657 to 1660 vertices

The present coloring was found on November 3, 2026, on an Apple M4 Mac mini. The search used the exact capacities of Remark 3.5, which include the antipodal rule, with all colors inside $T$ and all types free. In this setting the method of Appendix § 10.§ 1 did not converge, even with cardinality constraints, and served only to prove that some extensions are impossible; the coloring was found by local search instead. The local search changes one color inside $T$ or the type of one vertex at a time; it keeps a weight on each violated clique and raises the weights of cliques that stay violated, allows moves that leave the total weight unchanged, and uses a tabu list and random moves.

We started from the 81 vertices of $T$ in [5], moved the vertex $\bar{\imath}_7 = A_{675}$ from $V^{\circ}$ into $\Sigma$, so that it became a vertex of $T$ of its own type, and added one vertex at a time as a twin of an existing vertex: the twin has the type of its model, copies all its colors inside $T$ and is blue to it, and the local search then repaired the violated cliques. A twin of a vertex of type $c_{10} = b$ gave 1658 vertices after 105 seconds, and two twins of vertices of type $\bar{\imath}_7 = A_{675}$ gave 1659 and 1660 vertices after 438 and 428 seconds; the times are from the logs of these single runs. The local search changed types as well; only the final counts in Table 2 are claimed.

Negative results

We stop at 1660 vertices for the following reasons. All solver results below use the exact capacities of Remark 3.5, so an infeasible instance has no solution.

• 1661 vertices. From several 1660-vertex colorings, each with one twin added, the same local search found no 1661-vertex coloring. The best states, from four different starts, still had 3 violated cliques, and the longest runs stayed at 3 for several hours. In one of these states, all violated cliques are red and consist of vertices of types $a$ and $\bar{\imath}_7$ only.

• Many 1660-vertex colorings. Of 41 attempts that added a random twin to one of two 1659-vertex colorings, 21 gave a new 1660-vertex coloring within 15 minutes. Adding a further twin to these gave best states with 3 to 12 violated cliques. So 1660 vertices are easy to reach in this setting, and 1661 vertices are not.

• Exact repairs. On 23 colorings on 1660 vertices, the present one among them, we added one copy of a vertex of $\Sigma$ and freed the colors of all pairs inside $T$ with an endpoint in a set $U$ of 35 to 55 vertices of $T$ that contained the new vertex; all other colors inside $T$ and all types were kept. Of the 5,658 instances, which differ in the coloring, the type of the new vertex and $U$, the solver showed 5,532 infeasible; each of the others had $|U| \ge45$ and reached a time or memory limit. None gave a 1661-vertex coloring.

• More antipodes. Moving further antipodes into $\Sigma$ made the search worse: with the vertex $A_{760}$, the antipode of $i_{8}=B_{760}$, moved into $\Sigma$, the best state after an hour still had 8 violated cliques, and with the antipodes of all 17 vertices of $C \cup I$ whose antipodes lie in $V^{\circ}$ moved, it had 193 after half an hour.

• Without the second pair. With $\Sigma=C \cup I$ we found no $T$ of 82 vertices. Exact solver results rule out many local extensions of the 81-vertex set $T$ of [5]. For example, adding one vertex, with the types of the others kept, is infeasible for 13 of the 20 types of copies, even with all colors inside $T$ free; the other 7 cases were not decided, and a constant vertex cannot be added (Appendix § 10.§ 1). For two of the 13 infeasible cases the CNF was generated again by an independent program, a second solver also reported infeasibility, and a DRUP proof was checked by a separately written RUP checker.

The searches are heuristic; apart from the infeasibility results, they prove nothing.