#ramsey

First Lean 4 formalization of bipartite Ramsey b(2,2)=5 (Beineke-Schwenk 1976). Upper bound via native_decide over 2^25 ≈ 33M colorings. Mathlib v4.27 has no bipartite-Ramsey. Narvaez-Song-Zhang CICM 2024 covered classical Ramsey but not bipartite. Higher b(2,3)=9 and b(3,3)=17 stated as honest axioms (infeasible). Joins Papers 127 (Schur) and 128 (Davenport) as third small-value extremal-combinatorics Lean 4 first. 155 lines, 9 theorems, 0 sorry (2 axioms).