\pdfoutput=1
\documentclass[11pt]{article}

% ---------------------------------------------------------------- fonts & layout
\usepackage[T1]{fontenc}
\usepackage{amsmath,amsthm}
\usepackage{libertinus}
\usepackage{libertinust1math}
\usepackage[letterpaper,margin=1.05in]{geometry}
\usepackage{microtype}
\usepackage[table]{xcolor}
\usepackage{booktabs,array}
\usepackage{enumitem}
\usepackage{caption}
\usepackage{titlesec}
\usepackage{thmtools}
\usepackage{tikz}
\usepackage{needspace}

\definecolor{headcol}{RGB}{22,46,84}
\definecolor{accent}{RGB}{20,82,150}
\definecolor{rulecol}{RGB}{176,186,202}
\definecolor{rowcol}{RGB}{244,246,250}

\usepackage[colorlinks=true,linkcolor=accent,citecolor=accent,urlcolor=accent,hyperfootnotes=false,hypertexnames=false]{hyperref}
\hypersetup{pdftitle={R(12,12) >= 1661 by extending the Mathon-Shearer coloring},pdfauthor={Yue Ma}}
\usepackage[capitalise,nameinlink,noabbrev]{cleveref}
\crefname{appendix}{Appendix}{Appendices}
\crefname{subappendix}{Appendix}{Appendices}

\linespread{1.06}
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.5em plus 0.2em minus 0.1em}
\setlist{itemsep=0.2em,topsep=0.25em,parsep=0pt}
\setlist[itemize]{leftmargin=1.4em}
\setlist[enumerate]{leftmargin=2.1em}

\titleformat{\section}{\sffamily\bfseries\Large\color{headcol}}{\thesection}{0.8em}{}
\titleformat{\subsection}{\sffamily\bfseries\large\color{headcol}}{\thesubsection}{0.7em}{}
\titlespacing*{\section}{0pt}{2.4ex plus 1ex minus .3ex}{0.9ex}
\titlespacing*{\subsection}{0pt}{1.8ex plus .8ex minus .2ex}{0.5ex}
\titleformat{\paragraph}[runin]{\sffamily\bfseries\color{headcol}}{}{0pt}{}
\titlespacing*{\paragraph}{0pt}{1.4ex plus .6ex minus .2ex}{0.6em}
% fill a page before moving a section to the next one
\makeatletter\@secpenalty=-150\relax\makeatother

\captionsetup{font=small,labelfont={sf,bf,color=headcol},labelsep=period,skip=6pt}

% generous float placement, so that tables do not leave half-empty pages
\renewcommand{\topfraction}{0.9}
\renewcommand{\bottomfraction}{0.8}
\renewcommand{\textfraction}{0.07}
\renewcommand{\floatpagefraction}{0.85}
\setcounter{topnumber}{3}
\setcounter{bottomnumber}{2}
\setcounter{totalnumber}{4}

% statements upright; the bold sans head marks them
\declaretheoremstyle[headfont=\sffamily\bfseries\color{headcol},notefont=\sffamily\mdseries,
  notebraces={(}{)},bodyfont=\normalfont,spaceabove=0.55em,spacebelow=0.55em,headpunct={.},postheadspace=0.5em]{plainbody}
\declaretheorem[style=plainbody,numberwithin=section,name=Theorem]{theorem}
\declaretheorem[style=plainbody,sibling=theorem,name=Lemma]{lemma}
\declaretheorem[style=plainbody,sibling=theorem,name=Proposition]{proposition}
\declaretheorem[style=plainbody,sibling=theorem,name=Fact]{fact}
\declaretheorem[style=plainbody,sibling=theorem,name=Definition]{definition}
\declaretheorem[style=plainbody,sibling=theorem,name=Remark]{remark}

% proof head in bold sans instead of italics
\makeatletter
\renewenvironment{proof}[1][\proofname]{\par\pushQED{\qed}\normalfont
  \topsep4\p@\@plus4\p@\relax\trivlist
  \item[\hskip\labelsep\sffamily\bfseries\color{headcol}#1\@addpunct{.}]\ignorespaces}
  {\popQED\endtrivlist\@endpefalse}
% keep a short statement on the same page as its proof: \keepwithproof at the end of the
% statement, and keptproof instead of proof
\newcommand{\keepwithproof}{\@endparpenalty\@M}
\newenvironment{keptproof}{\@beginparpenalty\@M\begin{proof}}{\end{proof}}
\makeatother

% ---------------------------------------------------------------- notation
\newcommand{\term}[1]{\textbf{#1}}
\newcommand{\case}[1]{\textsf{\textbf{#1}}}
\newcommand{\M}{M}
\newcommand{\F}{\mathbb{F}}
\newcommand{\Vo}{V^{\circ}}
\newcommand{\cp}{\operatorname{cap}}
\newcommand{\Sg}{\Sigma}
% one entry of the contents box: reference, title, page
\newcommand{\tocrow}[2]{\cref{#1} & #2 & \pageref{#1}\\}

% ---------------------------------------------------------------- title block
\makeatletter
\renewcommand{\maketitle}{%
  \begin{center}
    {\sffamily\bfseries\LARGE\color{headcol}\boldmath
     $R(12,12)\ge 1661$ by extending\\[0.15em]
     the Mathon--Shearer coloring\par}
    \vspace{1.3em}
    {\large Yue Ma\par}
    \vspace{0.45em}
    {\small Department of Mathematics, Northeastern University\par
     Boston, MA 02115, USA\par
     \vspace{0.2em}
     \href{mailto:ma.yue6@northeastern.edu}{\texttt{ma.yue6@northeastern.edu}}\par}
  \end{center}
  \vspace{0.3em}}
\makeatother
\renewenvironment{abstract}
  {\begin{center}\begin{minipage}{0.87\textwidth}\small\linespread{1.05}\selectfont
   {\sffamily\bfseries\color{headcol}Abstract.}\enspace\ignorespaces}
  {\end{minipage}\end{center}\vspace{0.3em}}

\begin{document}

\maketitle

\begin{abstract}
We prove that $R(12,12)\ge1661$ by constructing a red/blue coloring of the edges of $K_{1660}$ with no monochromatic $K_{12}$.
We start from a classical $(11,11)$-coloring on $1596$ vertices, delete $21$ of its vertices and add $85$ new ones.
Toward the remaining $1575$ vertices, each new vertex has either the same colors as one of the deleted vertices or a single color.
The deleted vertices include two pairs whose members have complementary colors toward every other vertex, and these pairs weaken the conditions that the new vertices must satisfy.
The proof reduces to a finite check on the new vertices and is formally verified in Lean~4.
\end{abstract}

% subject classification as an unmarked footnote on the first page
{\renewcommand{\thefootnote}{}\footnotetext{2020 Mathematics Subject Classification: 05C55, 05D10.}}

% ================================================================
\section{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 \term{$(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~\cite{Rad} collects the known bounds.

For $R(12,12)$ the lower bound has improved in small steps.
Mathon~\cite{Mat} and Shearer~\cite{She} constructed an $(11,11)$-coloring on $1596$ vertices, which shows that $R(11,11)\ge1597$.
Xu, Shao and Radziszowski~\cite{XSR} 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$~\cite{Rad}.
In 2017, Tatarevic found a $(12,12)$-coloring on $1639$ vertices by a computer-assisted construction, so that $R(12,12)\ge1640$~\cite{T17}.
Tatarevic recently proved that $R(k+1,s+1)\ge R(k,s)+2k+2s$ for $5\le k\le s$~\cite{Tat}, 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$.

\begin{theorem}\label{thm:main}
There is a red/blue coloring of the edges of $K_{1660}$ with no monochromatic $K_{12}$. Hence $R(12,12)\ge 1661$.
\end{theorem}

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~\cite{Tat} 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$ (\cref{thm:criterion}); 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$ (\cref{lem:antipodal}).
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 (\cref{prop:rigid}).
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~\cite{Ma1642,Ma1658}, 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.
\Cref{app:found} 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 (\cref{lem:antipodal}) and a finite check that takes a computer about two seconds.
The result has also been checked by computer in several independent ways (\cref{app:verification}): two exhaustive searches by separate programs confirm that the coloring has no monochromatic $K_{12}$, and the theorem, including \cref{fact:mathon}, is formally verified in Lean~4.

% contents of the paper: two columns of equal width, three entries each, with page numbers
\noindent
\begin{tikzpicture}
\node[draw=rulecol, rounded corners=4pt, fill=rowcol, inner xsep=12pt, inner ysep=8pt,
      text width=\linewidth-24.8pt, align=center, font=\small] {%
  {\sffamily\bfseries\color{headcol}Contents}\par\smallskip
  \renewcommand{\arraystretch}{1.15}%
  \begin{tabular*}{0.46\linewidth}[t]{@{}>{\sffamily}l@{\hspace{0.7em}}l@{\extracolsep{\fill}}r@{}}
  \tocrow{sec:mathon}{The Mathon--Shearer coloring}
  \tocrow{sec:criterion}{The projection criterion}
  \tocrow{sec:coloring}{The coloring and Theorem~\ref*{thm:main}}
  \end{tabular*}\hfill
  \begin{tabular*}{0.46\linewidth}[t]{@{}>{\sffamily}l@{\hspace{0.7em}}l@{\extracolsep{\fill}}r@{}}
  \tocrow{sec:discussion}{Why an antipodal pair helps}
  \tocrow{app:verification}{Computer verification}
  \tocrow{app:found}{How the colorings were found}
  \end{tabular*}\par};
\end{tikzpicture}

% ================================================================
\section{The Mathon--Shearer coloring and its antipodes}\label{sec:mathon}

Let $q=797$, a prime with $q\equiv 1\pmod 4$, and let $S$ and $N$ be the nonzero squares and the nonsquares of $\F_q$; then $-1\in S$.
The coloring $\M=\M(797)$ has the $2q+2=1596$ vertices $A_x$, $B_x$ ($x\in\F_q$), $a$ and $b$; identifying $\F_q$ with $\{0,\dots,796\}$, we number them $A_x=x$, $B_x=797+x$, $a=1594$, $b=1595$:
\begin{itemize}
\item $A_xA_y$ and $B_xB_y$ are red if and only if $x-y\in S$;
\item $A_xB_y$ is red if and only if $x-y\in N$;
\item $a$ is red to every $A_x$, $b$ is red to every $B_x$, and all other pairs are blue.
\end{itemize}
We write $\M(u,v)$ for the color of $uv$.

\begin{fact}[Mathon~\cite{Mat}; Shearer~\cite{She}]\label{fact:mathon}
$\M(797)$ has no monochromatic $K_{11}$.
\end{fact}

The \term{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$.

\begin{lemma}\label{lem:antipodal}
For every vertex $v$ of $\M(797)$, the pair $v\bar v$ is blue, and $\M(v,w)\ne\M(\bar v,w)$ for every vertex $w\notin\{v,\bar v\}$.
\end{lemma}

\begin{proof}
The pairs $A_xB_x$ and $ab$ are blue by definition.
Since $-1\in S$, the sets $S$ and $N$ are closed under negation.
Take $v=A_x$.
For $w=A_y$ with $y\ne x$, the pair $A_xA_y$ is red if and only if $x-y\in S$, and $B_xA_y$ is red if and only if $y-x\in N$, that is, if and only if $x-y\notin S$.
For $w=B_y$ with $y\ne x$, the pair $A_xB_y$ is red if and only if $x-y\in N$, and $B_xB_y$ is red if and only if $x-y\in S$.
Finally, $a$ is red to $A_x$ and blue to $B_x$, and $b$ the other way round.
The case $v=B_x$ is the same.
For $v\in\{a,b\}$, the vertices $a$ and $b$ have different colors to every $A_x$ and every $B_x$.
\end{proof}

In the terminology of Mathon~\cite{Mat}, 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.

% ================================================================
\section{Clone extensions and the projection criterion}\label{sec:criterion}

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

\begin{definition}
Let $\Sg\subseteq V(\M)$ and $\Vo=V(\M)\setminus\Sg$.
A \term{typed set} is a finite set $T$ with a map $f\colon T\to\Sg\cup\{\mathrm{R},\mathrm{B}\}$; we call $f(t)$ the \term{type} of $t\in T$.
A \term{clone extension} is a red/blue coloring $\chi$ of the complete graph on $\Vo\sqcup T$ such that
\begin{itemize}
\item $\chi(u,v)=\M(u,v)$ for $u,v\in\Vo$;
\item for $t\in T$ and $v\in\Vo$: $\chi(t,v)=\M(f(t),v)$ if $f(t)\in\Sg$, red if $f(t)=\mathrm{R}$, and blue if $f(t)=\mathrm{B}$;
\item the colors of pairs inside $T$ are arbitrary.
\end{itemize}
The clone extension has $1596-|\Sg|+|T|$ vertices.
If $f(t)=g\in\Sg$, then $t$ has the colors of $g$ toward $\Vo$, and we call $t$ a \term{copy} of $g$.
If $f(t)=\mathrm{R}$ or $f(t)=\mathrm{B}$, then $t$ is red or blue to all of $\Vo$, and we call $t$ a \term{constant vertex} of color red or blue.
\end{definition}

For $K\subseteq T$ let $D(K)=f(K)\cap\Sg$ be the set of vertices of $\Sg$ copied by vertices of $K$.
For $D\subseteq\Sg$ let $\omega_c(D)$ be the largest number of vertices of $D$ that are pairwise $c$-adjacent in $\M$; the colors here are those of $\M$, not those of $\chi$.
An \term{antipodal pair} in $D$ is a pair $\{g,\bar g\}\subseteq D$.

\begin{lemma}\label{lem:projection}
Let $Q$ be a $c$-clique of a clone extension, $K=Q\cap T$ and $K^\circ=Q\cap\Vo$.
\begin{enumerate}[label=\textup{(\alph*)}]
\item If $K$ contains a constant vertex of color $\bar c$, then $K^\circ=\emptyset$.
\item If $D(K)$ contains an antipodal pair, then $K^\circ=\emptyset$.
\item In all cases $|K^\circ|\le 10-\omega_c(D(K))$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) A constant vertex of color $\bar c$ has color $\bar c$ to every vertex of $\Vo$, so no vertex of $\Vo$ lies in $Q$.
For (b) and (c), note that every vertex $v\in K^\circ$ is $c$-adjacent in $\M$ to every $g\in D(K)$: if $t\in K$ is a copy of $g$, then $\M(g,v)=\chi(t,v)=c$.
(b) If $g,\bar g\in D(K)$ and $v\in K^\circ$, then $v\notin\{g,\bar g\}$ because $v\in\Vo$, and $\M(g,v)=\M(\bar g,v)=c$ contradicts \cref{lem:antipodal}.
(c) Let $L\subseteq D(K)$ be a $c$-clique of $\M$ with $|L|=\omega_c(D(K))$.
Since $\chi=\M$ on $\Vo$, the set $K^\circ$ is a $c$-clique of $\M$, and it is disjoint from $L\subseteq\Sg$.
So $K^\circ\cup L$ is a $c$-clique of $\M$, and $|K^\circ|+|L|\le 10$ by \cref{fact:mathon}.
\end{proof}

\needspace{6\baselineskip}
For a color $c$ and $D\subseteq\Sg$, we define the \term{capacity function} $\cp_c$ by
\[
\cp_c(D)=\begin{cases}11&\text{if $D$ contains an antipodal pair,}\\ 1+\omega_c(D)&\text{otherwise.}\end{cases}
\]
We call the first case the \term{antipodal rule}.

\begin{theorem}\label{thm:criterion}
Let $\chi$ be a clone extension with typed set $T$, and suppose that, for each color $c$,
\begin{enumerate}[label=\textup{(\roman*)}]
\item $T$ contains no $c$-clique on $12$ vertices, and
\item every $c$-clique $K\subseteq T$ with no constant vertex of color $\bar c$ satisfies $|K|\le\cp_c(D(K))$.
\end{enumerate}
Then $\chi$ has no monochromatic $K_{12}$.
\end{theorem}

\begin{proof}
Let $Q$ be a $c$-clique and $K$, $K^\circ$ as in \cref{lem:projection}.
If $K=\emptyset$, then $Q$ is a $c$-clique of $\M$ and $|Q|\le 10$.
If $K$ contains a constant vertex of color $\bar c$, or $D(K)$ contains an antipodal pair, then $K^\circ=\emptyset$ and $|Q|=|K|\le 11$ by~(i).
Otherwise $|Q|=|K|+|K^\circ|\le(1+\omega_c(D(K)))+(10-\omega_c(D(K)))=11$ by~(ii) and \cref{lem:projection}(c).
\end{proof}

\begin{remark}\label{rem:allcliques}
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$ (\cref{app:found}).
\end{remark}

\begin{remark}\label{rem:exact}
Replacing the bound $10-\omega_c(D)$ of \cref{lem:projection}(c) by the exact value $e_c(D)$, the largest number of vertices of $\Vo$ that are pairwise $c$-adjacent in $\M$ and $c$-adjacent to every vertex of $D$, and hence $\cp_c(D)$ by the \term{exact capacity} $11-e_c(D)$, turns \cref{thm:criterion} into a necessary and sufficient condition, provided all cliques are checked.
Since $e_c(D)\le 10-\omega_c(D)$, and $e_c(D)=0$ by \cref{lem:antipodal} if $D$ contains an antipodal pair, the exact capacity is at least $\cp_c(D)$.
The search of \cref{app:ls} used the exact capacities; the coloring of \cref{sec:coloring} satisfies the conditions of \cref{thm:criterion} as stated, so its proof does not need them.
\end{remark}

% ================================================================
\section{The coloring}\label{sec:coloring}

Let $C=\{c_1,\dots,c_{10}\}$ and $I=\{i_1,\dots,i_{10}\}$ be the sets of vertices of $\M$ in \cref{tab:cliques}, given by name and by number (\cref{sec:mathon}).

\begin{table}[ht]
\centering
\small
\renewcommand{\arraystretch}{1.1}
\setlength{\tabcolsep}{4.6pt}
\begin{tabular}{@{}l*{10}{c}@{}}
\toprule
$p$ & $1$ & $2$ & $3$ & $4$ & $5$ & $6$ & $7$ & $8$ & $9$ & $10$\\
\midrule
$c_p$ & $B_{133}$ & $B_{129}$ & $B_{776}$ & $B_{541}$ & $B_{682}$ & $B_{686}$ & $B_{695}$ & $B_{785}$ & $B_{789}$ & $b$\\
 & $930$ & $926$ & $1573$ & $1338$ & $1479$ & $1483$ & $1492$ & $1582$ & $1586$ & $1595$\\
\addlinespace
$i_p$ & $B_{264}$ & $B_{791}$ & $B_{779}$ & $B_{752}$ & $B_{757}$ & $a$ & $B_{675}$ & $B_{760}$ & $B_{282}$ & $B_{470}$\\
 & $1061$ & $1588$ & $1576$ & $1549$ & $1554$ & $1594$ & $1472$ & $1557$ & $1079$ & $1267$\\
\bottomrule
\end{tabular}
\caption{The cliques $C$ and $I$: each vertex by name and, below it, by number.}
\label{tab:cliques}
\end{table}

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 $\Sg=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\imath_7=A_{675}$.
So $\Sg$ contains exactly two antipodal pairs: the pair $\{a,b\}=\{i_6,c_{10}\}$ inside $C\cup I$, and the new pair $\{i_7,\bar\imath_7\}$.
In all, $|\Sg|=21$ and $|\Vo|=1575$.
The $85$ vertices of $T$, their types and all colors inside $T$ were found by the computer search of \cref{app:ls}.

The file \texttt{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 $\Vo$ in increasing order, with the colors of $\M$.
Rows $1575$--$1659$ form $T$; their types are read from the file, and \cref{tab:types} 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.

\begin{table}[ht]
\centering
\small
\renewcommand{\arraystretch}{1.1}
\rowcolors{2}{rowcol}{white}
\begin{tabular}{@{}lc@{}}
\toprule
\textsf{\textbf{type}} & \textsf{\textbf{number of vertices}}\\
\midrule
constant red, constant blue & $11$ each\\
$i_7$ & $4$\\
$\bar\imath_7=A_{675}$ & $2$\\
each of the other $19$ vertices of $C\cup I$ & $3$\\
\midrule
total & $85$\\
\bottomrule
\end{tabular}
\caption{The types of the $85$ vertices of $T$.}
\label{tab:types}
\end{table}

\begin{theorem}\label{thm:coloring}
The coloring \texttt{r1212\_1660.graph} has no monochromatic $K_{12}$.\keepwithproof
\end{theorem}

\begin{keptproof}
The script \texttt{check\_antipodal\_projection.py} verifies that the file is a clone extension with the above $\Sg$: rows $0$--$1574$ equal $\M$ restricted to $\Vo$, rebuilt from the definition, and each of the $85$ other rows is, on $\Vo$, constant or equal to the row in $\M$ of exactly one $g\in\Sg$.
The script also checks \cref{lem:antipodal} 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 \cref{thm:criterion}: 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 $\Sg$; for each color, on $\Sg$ itself and on $200$ random subsets, they agree with those computed by the Python graph library \texttt{networkx}.
By \cref{thm:criterion}, the coloring has no monochromatic $K_{12}$.
\end{keptproof}

\Cref{thm:main} follows.
The antipodal rule is needed: with $\cp_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\imath_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)$.

% ================================================================
\section{Why an antipodal pair helps}\label{sec:discussion}

Condition~(ii) of \cref{thm:criterion} with $|D|\le 2$ already strongly limits the number of vertices of each type.

\begin{proposition}\label{prop:rigid}
Assume condition~(ii).
If $g\in\Sg$, the copies of $g$ span no monochromatic triangle, so there are at most $5$ of them.
If $g\ne h$ in $\Sg$ are not antipodal, the copies of $g$ and $h$ together span no $K_4$ in color $\M(g,h)$ and no triangle in the other color, so there are at most $8$ of them.
\end{proposition}

\begin{proof}
For both colors $\omega_c(\{g\})=1$, so $\cp_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 $\cp_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$~\cite{Rad}.
\end{proof}

In our earlier coloring on $1657$ vertices~\cite{Ma1658}, 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 $\Sg=C\cup I$ the exact values $e_c(D)$ of \cref{rem:exact} agree with $10-\omega_c(D)$ for $|D|\le 3$, 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, $\cp_c(\{g,\bar g\})=11$ and \cref{prop:rigid} gives no joint limit.
The present coloring improves on~\cite{Ma1658} at this point: its types $i_7$ and $\bar\imath_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 (\cref{sec:coloring}).
Since every vertex of $\M(797)$ has an antipode, any $g\in\Sg$ whose antipode lies in $\Vo$ can be given a partner by moving $\bar g$ into $\Sg$; 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 $\Sg=C\cup I$, our searches found no coloring on more than $1657$ vertices (\cref{app:neg}); 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 \cref{app:neg}.

% ================================================================
\section*{Data and code availability}
The $1660$-vertex coloring, the check script, checkers~A and~B (\cref{app:verification}), 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~\cite{repo}; \cref{app:verification} gives the hash of the coloring and the archived versions.
The programs and logs of the searches in \cref{app:found} are not public.

\section*{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~\cite{Ma1658}, 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 \texttt{nanoda}, and on the exhaustive searches (\cref{app:verification}).

\section*{Acknowledgments}
The author thanks Milos Tatarevic for publishing the paper~\cite{Tat} together with the Lean development and programs~\cite{T26code}, on which the formal proof builds, and Stanis\l{}aw Radziszowski for many years of attention to these questions and for collecting the known bounds in~\cite{Rad}; both answered the author's messages with encouragement.
Thanks also go to G\'abor Lippner, 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.

% ================================================================
% the appendices start on a new page
\clearpage
\appendix
\crefalias{section}{appendix}
\crefalias{subsection}{subappendix}

\section{Computer verification}\label{app:verification}

The proof of \cref{thm:coloring} rests on one finite computation, the check of \cref{thm:criterion}.
\Cref{tab:checks} lists this check together with the independent ones.
The two exhaustive searches use no structure of the coloring and do not depend on \cref{fact:mathon}.
The other checks depend on \cref{fact:mathon}; they come from three programs, written separately, in different sessions of the AI system: the check script of \cref{thm:coloring} 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~\cite{repo}.

\begin{table}[ht]
\centering
\small
\renewcommand{\arraystretch}{1.1}
\rowcolors{2}{rowcol}{white}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{5.0cm}>{\raggedright\arraybackslash}p{5.4cm}>{\raggedright\arraybackslash}p{4.6cm}@{}}
\toprule
\textsf{\textbf{check}} & \textsf{\textbf{method}} & \textsf{\textbf{result}}\\
\midrule
exhaustive search, program of~\cite{Ma1642} (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\\
\texttt{check\_antipodal\_\allowbreak projection.py} (this paper) & \cref{thm:criterion}, all cliques & PASS; $1.8$\,s, one thread\\
checker A, bound mode & \cref{thm:criterion}, all cliques & PASS; clique counts and histograms of $\cp_c(D(K))-|K|$ identical to the script's\\
checkers A and B, exact mode & \cref{rem:exact}, all cliques, $e_c$ computed exactly & both PASS\\
\bottomrule
\end{tabular}
\caption{Checks of \texttt{r1212\_1660.graph}. The first search ran on an Apple M4 Mac mini with 5 threads from 13:16 to 16:22 EST on November 3, 2026, the second on the same computer with 8 threads from 17:18 to 19:33 EST. The output of the first was checked by the output checker of~\cite{Ma1658}, that of the second by its own checker; both checks passed. The longest tasks took $170$\,s and $140$\,s.}
\label{tab:checks}
\end{table}

\paragraph{Controls.}
The following controls test the checks themselves.
\begin{itemize}
\item \case{Flipped edge.} Flipping the color of the edge between the constant red vertices in rows $1615$ and $1616$ makes \texttt{check\_antipodal\_projection.py} report two violated cliques, with $D=\emptyset$ 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.
\item \case{No antipodal rule.} Without the rule, the same script fails with $5{,}332$ violations, as in \cref{sec:coloring}. Checker~A in bound mode, without the rule, reports the same number.
\item \case{Structure.} Flipping an edge inside $\Vo$, or between $T$ and $\Vo$, makes the script stop with an error.
\item \case{Search programs.} Both exhaustive programs were tested on November 3, 2026, when we reverified~\cite{Ma1658}: the first reproduced the published run of~\cite{Ma1658} 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.
\end{itemize}

\needspace{5\baselineskip}
\paragraph{Formal proof in Lean.}
We have formalized \cref{thm:main} in Lean~4 (version 4.32.1) with Mathlib~\cite{dMU21,mathlib}:
\begin{center}\small
\texttt{theorem RamseyIncrement.R1661.r1212\_lower\_bound : 1661 $\le$ ramseyNumber 12 12}
\end{center}
\begin{itemize}
\item \case{The statement.} \texttt{ramseyNumber} is the definition of~\cite{Ma1642,Ma1658}, from Tatarevic's Lean development~\cite{T26code}: 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 \texttt{Fin 1660} and its complement. The coloring is defined on $\Vo\sqcup\{0,\dots,84\}$, with tables generated from the graph file.
\item \case{The argument} follows \cref{thm:criterion}. The proof uses \cref{fact:mathon}, proved in Lean in~\cite{Ma1642}; \cref{lem:antipodal}, proved in Lean from $-1\in S$; the colors of $\M$ on $\Sg$; 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 \cref{lem:projection}, 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~\cite{Ma1658}, applied to $T$ with the edges between copies of antipodal types removed. These checks cover every such clique, not only the maximal ones, so \cref{rem:allcliques} causes no difficulty. The proof does not use the exhaustive searches.
\item \case{Axioms:} only \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}. No \texttt{sorry}, no \texttt{native\_decide}.
\item \case{Independent kernels.} \texttt{leanchecker} replayed each of the $25$ modules of the proof separately, and \texttt{nanoda}~\cite{nanoda}, a Lean kernel written separately in Rust, checked an export of the theorem made with \texttt{lean4export}~\cite{lean4export}, together with all $29{,}313$ declarations it uses, Mathlib included. Both accepted the proof. As a control, \texttt{nanoda} rejected a copy with one bit of a table changed. Of the $25$ modules, $19$ come unchanged from~\cite{Ma1642} and one, the defect lemma, from~\cite{Ma1658}; $5$ are new.
\item \case{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.
\end{itemize}

\paragraph{Data.}
The coloring is the file \texttt{graph/r1212\_1660.graph} in~\cite{repo}, in the format of \cref{sec:coloring}: $1660$ lines of $1660$ characters, $2{,}757{,}260$ bytes.
The numbering of the vertices of $\M$ in \cref{sec:mathon} is the same as in the files of~\cite{Ma1642,Ma1658}; the rows of the present file are ordered as in \cref{sec:coloring}.
The SHA-256 hash of the file is
\begin{center}\small
\texttt{07c5cbb696c1d7662870b42e6a1c508e7ef46bf2313f01d297f914e62448867d}.
\end{center}
Version~1.0.1 of the repository is archived at \url{https://doi.org/10.5281/zenodo.24087657}, and \url{https://doi.org/10.5281/zenodo.23963534} refers to all versions.
The files of the repository and of~\cite{Ma1642,Ma1658} 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 \texttt{i6bar} in the outputs of the repository stands for $\bar\imath_7$.
The repository also lists the type of every vertex of $T$.

\section{How the colorings were found}\label{app:found}

\Cref{tab:history} lists our colorings, together with the one given by Tatarevic's construction.
All of them have the shape of \cref{sec:criterion}: they consist of $\Vo$ and a typed set $T$, and each vertex of $T$ copies a vertex of $\Sg$ or has a single color toward $\Vo$.
Except in the last row, $\Sg=C\cup I$, so that $|\Vo|=1576$, and $T$ contains the $20$ vertices of $C\cup I$, as copies of themselves with the colors of $\M$ among them.
This $\Sg$ already contains the antipodal pair $\{a,b\}=\{i_6,c_{10}\}$, but the proofs of~\cite{Ma1642,Ma1658} do not use it.

\begin{table}[ht]
\centering
\small
\renewcommand{\arraystretch}{1.1}
\rowcolors{2}{rowcol}{white}
\begin{tabular}{@{}cccll@{}}
\toprule
\textsf{\textbf{bound}} & $|\Vo|$ & $|T|$ & \textsf{\textbf{new ingredient}} & \textsf{\textbf{source}}\\
\midrule
$1641$ & $1576$ & $64$ & Tatarevic's construction applied to $C$ and $I$ & \cite{Tat}\\
$1642$ & $1576$ & $65$ & one more vertex after recoloring $7$ pairs & \cite{Ma1642}\\
$1651$ & $1576$ & $74$ & colors inside $T$ found by a SAT solver & not released\\
$1658$ & $1576$ & $81$ & the solver also chooses what each vertex copies & \cite{Ma1658}\\
$1661$ & $1575$ & $85$ & a second antipodal pair; local search & this paper\\
\bottomrule
\end{tabular}
\caption{Colorings of $K_n$ with no monochromatic $K_{12}$ built from the Mathon--Shearer coloring, where $n=|\Vo|+|T|$ and the bound is $R(12,12)\ge n+1$. In all but the last, $T$ contains $C\cup I$ with the colors of the Mathon--Shearer coloring among these $20$ vertices; in the last, all colors inside $T$ are free.}
\label{tab:history}
\end{table}

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 $\Vo$, so that $|T|=64$.
In~\cite{Ma1642}, recoloring $7$ pairs inside $T$ made room for one more vertex, so that $|T|=65$.
The release~\cite{Ma1642} used \cref{thm:criterion}, 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 \cref{app:verification}.

\paragraph{Maximal cliques.}
Without the antipodal rule, that is, with $\cp_c(D)=1+\omega_c(D)$ for all $D$, condition~(ii) of \cref{thm:criterion} 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~\cite{Ma1642,Ma1658} and the searches of \cref{app:sat} rely on this.
With the antipodal rule the slack can increase (\cref{rem:allcliques}): if $K$ contains copies of $g$ but none of $\bar g$, adding a copy of $\bar g$ raises the capacity to $11$.

\subsection{From 1641 to 1657 vertices}\label{app:sat}

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

\paragraph{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|\ge 12$, 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~\cite{Ma1642}.

\paragraph{1650 vertices.}
Starting from the $45$ new vertices of~\cite{Ma1642}, 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~\cite{Ma1642} 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 $54$th.
The $54$ new vertices are $11$ constant red, $11$ constant blue and $32$ copies; the constant vertices are those of~\cite{Ma1642}.
For a $55$th vertex, every choice timed out except one, which the solver reported infeasible.

\paragraph{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 \cref{prop:rigid} 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 $\cp_c(\emptyset)=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~\cite{cadical}, called through PySAT~\cite{pysat}, each step added one vertex.
From $54$ to $60$ new vertices the steps took between $10$ seconds and $18$ minutes, and the $61$st vertex took $21$ minutes.
For a $62$nd 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.

\subsection{From 1657 to 1660 vertices}\label{app:ls}

The present coloring was found on November 3, 2026, on an Apple M4 Mac mini.
The search used the exact capacities of \cref{rem:exact}, which include the antipodal rule, with all colors inside $T$ and all types free.
In this setting the method of \cref{app:sat} 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~\cite{Ma1658}, moved the vertex $\bar\imath_7=A_{675}$ from $\Vo$ into $\Sg$, 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 \cref{tab:types} are claimed.

\subsection{Negative results}\label{app:neg}

We stop at $1660$ vertices for the following reasons.
All solver results below use the exact capacities of \cref{rem:exact}, so an infeasible instance has no solution.
\begin{itemize}
\item \case{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.
\item \case{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.
\item \case{Exact repairs.} On $23$ colorings on $1660$ vertices, the present one among them, we added one copy of a vertex of $\Sg$ 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.
\item \case{More antipodes.} Moving further antipodes into $\Sg$ made the search worse: with the vertex $A_{760}$, the antipode of $i_8=B_{760}$, moved into $\Sg$, 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 $\Vo$ moved, it had $193$ after half an hour.
\item \case{Without the second pair.} With $\Sg=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~\cite{Ma1658}. 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 (\cref{app:sat}). 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.
\end{itemize}
The searches are heuristic; apart from the infeasibility results, they prove nothing.

% ================================================================
% keep the heading with the first few entries
\needspace{8\baselineskip}
\begin{thebibliography}{99}
\setlength{\itemsep}{0pt}
\small
% addresses in the text font here, so that each repository entry fits on two lines
\urlstyle{same}

\bibitem{cadical}
CaDiCaL SAT solver, \url{https://github.com/arminbiere/cadical}.

\bibitem{dMU21}
L.~de~Moura and S.~Ullrich, The Lean~4 theorem prover and programming language, in \emph{Automated Deduction -- CADE 28}, Lecture Notes in Computer Science 12699, Springer, 2021, 625--635.

\bibitem{lean4export}
lean4export: plain-text declaration export for Lean~4, \url{https://github.com/leanprover/lean4export}.

\bibitem{Ma1642}
Y.~Ma, $R(12,12)\ge1642$: a colouring of $K_{1641}$, a Lean proof and computer checks, software repository, 2026, \url{https://github.com/YueMa0/r1212-1642}, archived at \url{https://doi.org/10.5281/zenodo.23770924}.

\bibitem{Ma1658}
Y.~Ma, $R(12,12)\ge1658$: a colouring of $K_{1657}$, a Lean proof and computer checks, software repository, 2026, \url{https://github.com/YueMa0/r1212-1658}, archived at \url{https://doi.org/10.5281/zenodo.23827702}.

\bibitem{repo}
Y.~Ma, $R(12,12)\ge1661$: a colouring of $K_{1660}$, a Lean proof and computer checks, software repository, 2026, \url{https://github.com/YueMa0/r1212-1661}, archived at \url{https://doi.org/10.5281/zenodo.23963534}.

\bibitem{Mat}
R.~Mathon, Lower bounds for Ramsey numbers and association schemes, \emph{J. Combin. Theory Ser.~B} \textbf{42} (1987), 122--127.

\bibitem{mathlib}
The mathlib Community, The Lean mathematical library, in \emph{Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)}, ACM, 2020, 367--381.

\bibitem{nanoda}
nanoda\_lib: a type checker for Lean~4, \url{https://github.com/ammkrn/nanoda_lib}.

\bibitem{pysat}
PySAT: a toolkit for SAT-based prototyping in Python, \url{https://github.com/pysathq/pysat}.

\bibitem{Rad}
S.~P.~Radziszowski, Small Ramsey numbers, \emph{Electron. J. Combin.}, Dynamic Survey DS1, revision~18, April 24, 2026.

\bibitem{She}
J.~B.~Shearer, Lower bounds for small diagonal Ramsey numbers, \emph{J. Combin. Theory Ser.~A} \textbf{42} (1986), 302--304.

\bibitem{T17}
M.~Tatarevic, On the Ramsey number $R(12,12)$, research note, February 14, 2017, \url{https://mtatar.wordpress.com/2017/02/14/r12/}.

\bibitem{Tat}
M.~Tatarevic, A constructive two-parameter Ramsey increment, \href{https://arxiv.org/abs/2608.06531}{arXiv:2608.06531}, 2026.

\bibitem{T26code}
M.~Tatarevic, Ramsey increment theorem: Lean formalization, executable construction, and graph certificates, software repository, 2026, \url{https://github.com/milostatarevic/ramsey-increment-theorem}.

\bibitem{XSR}
X.~Xu, Z.~Shao and S.~P.~Radziszowski, More constructive lower bounds on classical Ramsey numbers, \emph{SIAM J. Discrete Math.} \textbf{25} (2011), 394--400.

\end{thebibliography}

\end{document}