AI 中文总结
该研究构造性证明了经典拉姆齐数的双参数不等式，在Lean 4中形式化其证明，得到拉姆齐数R(12,12)的新下界为1641。
AI 中文摘要
我们证明了经典拉姆齐数满足不等式 $R(k+1,s+1) \ge R(k,s) + 2k + 2s$，该式对所有 $5 \le k \le s$ 均成立，并在 Lean 4 中形式化了该证明。由此得到新下界 $R(12,12) \ge 1641$。
英文摘要
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$.
