The Ramsey problem R(3,k) seeks to determine the smallest value of n such that any red/blue edge coloring of the complete graph on n vertices must either contain a blue triangle (3-clique) or a red clique of size k. Despite its significance, many previous computational results for the Ramsey R(3,k) problem such as R(3,8) and R(3,9) lack formal verification. To address this issue, we use the software MathCheck to generate certificates for Ramsey problems R(3,8) and R(3,9) (and symmetrically R(8,3) and R(9,3)) by integrating a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). Our SAT+CAS approach significantly outperforms traditional SAT-only methods, demonstrating an improvement of several orders of magnitude in runtime. For instance, our SAT+CAS approach solves R(3,8) (resp., R(8,3)) sequentially in 59 hours (resp., in 11 hours), while a SAT-only approach using state-of-the-art CaDiCaL solver times out after 7 days. Additionally, in order to be able to scale to harder Ramsey problems R(3,9) and R(9,3) we further optimized our SAT+CAS tool using a parallelized cube-and-conquer approach. Our results provide the first independently verifiable certificates for these Ramsey numbers, ensuring both correctness and completeness of the exhaustive search process of our SAT+CAS tool.

The Ramsey problem R(3,8) asks for the smallest n such that every red/blue coloring of the complete graph on n vertices must contain either a blue triangle or a red 8-clique. We provide the first certifiable proof that R(3,8) = 28, automatically generated by a combination of Boolean satisfiability (SAT) solver and a computer algebra system (CAS). This SAT+CAS combination is significantly faster than a SAT-only approach. While the R(3,8) problem was first computationally solved by McKay and Min in 1992, it was not a verifiable proof. The SAT+CAS method that we use for our proof is very general and can be applied to a wide variety of combinatorial problems.