  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.
