myy555/CombiBench

CombiBench是第一个专注于组合数学问题的基准测试，基于Lean 4形式语言。该数据集是一个手工制作的基准，包含100个不同难度和知识水平的组合数学问题，旨在为评估自动定理证明系统的组合数学能力提供基准。数据集的问题来源多样，包括IMO、Brualdi的书、Hackmath等，涵盖了从中学水平到高级数学竞赛的广泛问题。

CombiBench is the first benchmark focused on combinatorial problems, based on the formal language Lean 4. It is a manually produced benchmark including 100 combinatorial mathematics problems of varying difficulty and knowledge levels, aimed at providing a benchmark for evaluating the combinatorial mathematics capabilities of automated theorem proving systems. The dataset features a diverse range of problem sources, including IMO, Brualdis book, Hackmath, etc., covering a wide spectrum from middle school level to advanced mathematical competitions.