Formalizing Finite Ramsey Theory in Lean 4

Ramsey theory is arguably one of the most beautiful and challenging areas in combinatorics. In formal mathematics, Ramsey’s (infinite) theorem is a popular benchmark for interactive theorem provers (ITPs) and many applications of finite Ramsey theory are found in automated reasoning (AR). Nevertheless, to the best of our knowledge there is no single theory collecting all current knowledge on small Ramsey numbers in a way that resembles the conventional didactic approach. We set out to fill this gap by exploiting Lean 4’s flexibility to incorporate results from interactive and automated theorem proving. We prove exact values for several small Ramsey numbers and related van der Waerden numbers. In doing so, we also highlight pain points in using ITPs for combinatorics and graph theory and develop tactics and widgets to alleviate some of these issues.