Summary (Overview)

• Main Result: The paper improves the upper bound on the classical Ramsey number $R(3,3,3,3)$ from 62 to 61, proving that every 4-coloring of the edges of $K_{61}$ contains a monochromatic triangle.
• Methodology: The proof combines combinatorial reasoning (ticket counting, neighborhood classifications) with exhaustive SAT solving—56,723 formulas in total were refuted by two independent SAT solvers.
• Formal Verification: The mathematical reductions are formalized in the Lean 4 proof assistant, with the final theorem UniformK61.WholeProof.ramsey61 depending only on the unsatisfiability of the SAT formulas.
• Key Innovation: The proof introduces the concepts of "tickets" (counting critical neighborhood interactions), "entrances" (special structural configurations), and "perfect balance" to decompose the problem into tractable cases.
• Computational Scale: The SAT computations required approximately 677 CPU hours using Kissat 4.0.4 and CaDiCaL 3.0.1 solvers on an Apple M4 Max machine.

Introduction and Theoretical Foundation

The Ramsey number $R(k_1, \ldots, k_q)$ is defined as the least integer $n$ such that every $q$-coloring of the edges of $K_n$ contains a monochromatic $K_{k_i}$ in color $i$ for some $i$. A good coloring is one with no monochromatic triangle.

The previous best upper bound was $R(3,3,3,3) \leq 62$, established by Fettes, Kramer, and Radziszowski. The lower bound was $51$, giving a gap of 11 to close.

The proof strategy begins by considering a vertex $r$ and its four color neighborhoods $N_i(r)$. Since $R(3,3,3) = 17$, each color neighborhood of a good coloring can have at most 16 vertices (as an edge of color $i$ inside $N_i(r)$ would form a monochromatic triangle with $r$). The four color degrees sum to 60, and their deficits from 16 sum to 4, giving exactly five possible profiles:

A key structural result (Theorem 2.1, due to Kalbfleisch, Stanton, and Heinrich) classifies good 3-colorings of $K_{16}$: there are exactly two, called the untwisted template U and twisted template T (up to relabeling and color permutation). Good 3-colorings of $K_{15}$ are obtained by deleting a vertex from U or T.

Methodology

Ticket Counting

The paper introduces a "ticket" metaphor: vertex $u$ sends a ticket to $v \neq u$ when $d_{c(uv)}(u) \geq 15$ (i.e., the color of edge $uv$ is critical at $u$). The number of tickets sent by vertex $v$ is:

$$w(v) = \sum_{i: d_i(v) \geq 15} d_i(v)$$

and the number received is:

$$H(v) = |\{u \neq v : d_{c(uv)}(u) \geq 15\}|$$

Double counting gives the crucial identity:

$$\sum_{v} H(v) = \sum_{v} w(v) \tag{2}$$

The A, B, D Bounds via Marked Neighborhoods

For profiles A, B, and D, the paper proves (Proposition 2.4) that a vertex receives strictly fewer tickets than it sends. The approach:

1. If a root $r$ of profile A, B, or D receives too many tickets, at least 4, 3, or 2 of them (respectively) must come from a specific 16-vertex group $R_3$.
2. Choose such a sender as the mark $p$. Its critical neighborhood $S = N_3(p)$ (the brace) contains $r$ and must avoid $R_3$.
3. The brace intersects the other three groups in supports $S_i = S \cap R_i$ with sizes $(|S_0|, |S_1|, |S_2|)$ of shape $(4,5,5)$, $(5,4,5)$, $(5,5,4)$, or $(5,5,5)$.
4. Since each support carries a good 2-coloring (as edges avoid two colors and $R(3,3) = 6$), supports of size 5 carry complementary 5-cycles, and size-4 supports carry complementary paths.
5. For each shape, exactly 600 distinct "words" describe how the brace's template colors the edges between supports.
6. Normalized configurations are built by placing supports on fixed vertices, with sym