A Formal Proof of R(4,5)=25

TL;DR

We address the decision problem $R(4,5)=25$ by providing a formal HOL4 proof that combines a high-level splitting argument with SAT-backed gluing lemmas. The key innovation is a verified generalization algorithm that reduces the search space and a simplicity heuristic that predicts SAT-solving difficulty, enabling a feasible, fully formalized verification. The authors rely on the HOL4 interface to MiniSat to prove gluing lemmas rather than reimplementing a solver, and they demonstrate the existence of a $\mathcal{R}(4,5,24)$-graph to establish the lower bound. This work advances formalizations in finite Ramsey theory and illustrates practical strategies for certifying large computational proofs.

Abstract

In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat SAT to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.

Figures (6)

• Figure 1: Neighbors (blue-neighbors) and antineighbors (red-neighbors) of a vertex of degree d in an $\mathcal{R}(4,5,25)$-graph.
• Figure 2: Construction of an exact cover $\mathcal{G^*}$ of a set of graphs $\mathcal{G}$. The process of graying edges stops as it would otherwise produce a gray triangle including a blue triangle. The construction of an exact cover terminates in this case after one iteration. The dotted arrows indicate which graph belongs to which generalization.
• Figure 3: Extension of an $\mathcal{R}^*(3,5,9)$-generalization depicted as an adjacency matrix. The first 9 rows and columns represent the vertices $x_0$ to $x_8$ of the $\mathcal{R}^*(3,5,9)$-generalization. Gray edges are represented by dotted gray circles. Edges containing the extension vertex $x_9$ (last row and column) are represented by black circles.
• Figure 4: The adjacency matrix of a graph of size 24 where a partial coloring is given by a generalization $G^*$ with 4 gray edges (dotted gray circles) with vertices numbered from 0 to 9 and a generalization $H^*$ with 4 gray edges with vertices numbered from 10 to 23. The goal of the SAT solvers is to prove that there is no way to assign a color (blue or red) to the gray edges and the transverse edges (black circles) without creating a blue 4-clique or a red 5-clique.
• Figure 5: The five possible types of configurations. In each configuration, a colored clique in an $\mathcal{R}(3,5,d)$-graph is displayed on the left and a colored clique in an $\mathcal{R}(4,4,24-d)$-graph is displayed on the right. Transverse edges are shown as dotted black edges. Transverse edges must not all be blue in blue configurations and they must not all be red in red configurations.

Theorems & Definitions (9)

• Remark
• Definition 1
• Definition 2
• Definition 3
• Lemma 4
• Lemma 5
• Lemma 6
• Lemma 7
• Definition 8