A constructive two-parameter Ramsey increment

Abstract

We prove the inequality $R(k+1,s+1)\ge R(k,s)+2k+2s$ for classical Ramsey numbers, valid for all $5\le k\le s$, and formalize the proof in Lean 4. As a consequence, we obtain the new lower bound $R(12,12)\ge 1641$.