#combinatorics

Partial Lean 4 formalization of classical Sylvester-Schur (Erdos 699 binomial form + Erdos 961 consecutive-integer form). 15 verified theorems: exact k=1 and k=2 cases, Bertrand-boundary m=k+1 for all k, native_decide bounded cases k in {3..10} and m<=200 (1552 finite cases), fully verified conditional 699-to-961 reduction via ascFactorial. 1 honest core sorry (k>=3 arbitrary m needs Erdos 1934, not attempted). Option-B follow-up to Paper 132 Part F.4 structural lesson.

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).

First Lean 4 formalization of the Davenport constant D(G) for finite abelian groups. Certifies D(Z3)=3, D(Z4)=4, D(Z5)=5 (cyclic, Davenport 1966) and D(Z2 x Z2)=3 (non-cyclic, Olson 1969) via native_decide over 3,472 sequence-enumeration cases plus witness checks. The EGZ-Davenport bridge E(G) = D(G) + |G| - 1 (Gao 1996) is verified by decide for n in {3,4,5}. Mathlib v4.27 contains Cauchy-Davenport but lacks D(G); Paper 128 with Paper 127 constitute the first Lean 4 advance in small-exact-value zero-sum combinatorics since Narvaez-Song-Zhang CICM 2024.

First Lean 4 formalization of Schur S(2)=4, S(3)>=13, S(4)>=44 (OEIS A030126) plus tightness witnesses for Erdos-Ginzburg-Ziv E(Z3)=5, E(Z4)=7 complementing Mathlib's general theorem. 17,174 native_decide enumerations. W(3;2)=9 re-derived (subsumed by Narvaez CICM 2024). First paper adopting Template v3 (VERIFIED / EMPIRICAL / AXIOMATIC separation).

The first six rows of Pascal's triangle, in all their glory! Pascal's triangle's beauty is in...

How to split a quantity unequally