Combinatorics Benchmark in Lean 4

Stream: Machine Learning for Theorem Proving

[Mert Ünsal]

It seems that competition-style combinatorics problems are hard to formalize and prove in Lean 4 - is there any benchmark that has a good number of combinatorics problems?

From what I understand minif2f doesn't have any combinatorics problems, FIMO is just algebra and number theory. PutnamBench has 29 combinatorics problems.