AI-MO/CombiBench
CombiBench CombiBench is the first benchmark focused on combinatorial problems, based on the formal language Lean 4. CombiBench is a manually produced benchmark, including 100 combinatorial mathematics problems of varying difficulty and knowledge levels. It aims to provide a benchmark for evaluating the combinatorial mathematics capabilities of automated theorem proving systems to advance the field. For problems that require providing a solution first and… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/CombiBench.
CombiBench
<p align="center"> <a href="https://github.com/MoonshotAI/CombiBench/"><img src="https://img.shields.io/badge/🚀-github-black"</a> </p>
##
CombiBench is the first benchmark focused on combinatorial problems, based on the formal language Lean 4. CombiBench is a manually produced benchmark, including 100 combinatorial mathematics problems of varying difficulty and knowledge levels. It aims to provide a benchmark for evaluating the combinatorial mathematics capabilities of automated theorem proving systems to advance the field. For problems that require providing a solution first and then proving its correctness, we have referred to the style of PutnamBench.
We are hosting a **leaderboard** and will readily receive evaluation results which are accompanied by a preprint or publication. Please reach out privately at liujunqi@amss.ac.cn with any requests for additions to the leaderboard.
Statistics
We collected all combinatorics problems from the official IMO problems since 2000, except for one problem that relies on a figure. And We selected problems through random sampling from 14 chapters in the book, choosing 3 problems from each chapter, ensuring that the 42 problems are evenly distributed across all 14 chapters. We randomly selected 10 simple combinatorics problems at the middle school level from a mathematics problem collection website hackmath. Then, we randomly collected 12 problems from other mathematics competitions.
Note : The complete proofs of Problem 3 and Problem 5 from IMO 2024 have already been formalized in mathlib4/Archive/Imo2024Q3 and mathlib4/Archive/Imo2024Q5. Therefore, we directly refer to the statements of these problems, along with the necessary definitions used in the statements. We are very grateful to Joseph Myers, the author of these two problems. We also appreciate his suggestions on the formalization of our problems.
Evaluation
Our evaluation code is released at https://github.com/MoonshotAI/CombiBench
🙌 Contributing
Contributions are welcome! If anyone notices any mistakes, please raise an issue on the repository and we will address it.
📝 License
This project is licensed under the MIT License. See the LICENSE file for full details.