Combinatorics · AI-MO
CombiBench
A Lean 4 benchmark of 100 formalised combinatorial mathematics problems for automated theorem proving systems.
What CombiBench is
CombiBench is a benchmark focused on combinatorial problems, formalised using the Lean 4 interactive theorem prover. Developed by AI-MO, it comprises 100 manually curated combinatorial mathematics problems designed to assess and advance the discrete-reasoning capabilities of automated theorem proving systems and language models.
The dataset spans a range of difficulty and knowledge requirements, from middle school exercises to advanced mathematical olympiad challenges. For problems requiring an agent to propose a solution prior to proving its correctness, the formulation adopts the style used in PutnamBench.
How it was made
CombiBench was constructed through manual formalisation of 100 mathematical problems into Lean 4. The dataset includes all combinatorics problems from the official International Mathematical Olympiad (IMO) since 2000, excluding a single problem that depends on a figure. Additionally, 42 problems were gathered via random sampling across 14 chapters of Brualdi's textbook (three problems per chapter), 10 introductory problems were sampled from the Hackmath collection, and 12 problems were collected from other competitions including APMO, Baltic Way, EGMO, IMO Shortlist, IZHO, BXMO, and USAMO.
For certain IMO problems—such as Problem 3 and Problem 5 from IMO 2024—the benchmark incorporates existing problem statements and formal definitions established in Lean 4's mathlib archive.
Key facts
- Publisher
- AI-MO
- Number of problems
- 100
- Formal language
- Lean 4
- Format
- Parquet
- Modality
- Text
- Domain
- Combinatorics and discrete mathematics
- Release date
- 9 March 2025
What you can use it for
- Automated theorem proving evaluation
- Benchmarking automated theorem provers and proof-search agents on formal combinatorics proofs in Lean 4.
- Mathematical reasoning in language models
- Evaluating the capacity of large language models to generate solutions and formal proofs for discrete-mathematics competition problems.
- Combined solution finding and proof verification
- Testing systems on two-stage problems that require predicting a discrete solution and formally verifying its correctness.
Explore the data
The schema, real rows, full-text search and a SQL filter — read in your browser, nothing downloaded.
Explore
Read the real rows without downloading anything
Reading rows…
LiveRead from AI-MO/CombiBench at the moment you asked. Nothing is cached or stored — every row above came from that request.
How the columns are distributed
Over 100 rows of default/test
answer
list- min
- 1
- median
- 1
- mean
- 1.04
- max
- 3
55.0% empty
formal_statement
string_text- min
- 93
- median
- 417
- mean
- 622.92
- max
- 3,054
natural_language
string_text- min
- 48
- median
- 260
- mean
- 343.46
- max
- 1,246
source
string_label- https://www.hackmath.net/en/word-math-problems/combinatorics10%
90.0% empty
tag
string_label- brualdi42%
- imo36%
- math_competitions12%
theorem_name
string_text- min
- 10
- median
- 12
- mean
- 12.41
- max
- 17
Strengths and limits
Good at
- It is the first benchmark focused specifically on combinatorial mathematics formalised in Lean 4.
- The problems are manually formalised across varied difficulty levels, from secondary school exercises to IMO competition standards.
- Coverage includes an even distribution of 42 problems across 14 distinct chapters of Brualdi's combinatorics textbook.
Watch out for
- It omits problems that rely on visual figures, including one post-2000 IMO combinatorics problem.
- With 100 formalised problems, the total benchmark size is relatively small.
Questions
Can I look inside CombiBench without downloading it?
Yes. This page reads its schema, real rows and per-column statistics in the browser, with full-text search and a SQL filter. Nothing is downloaded to your machine.
What licence is CombiBench under?
Its authors declare mit. Read the terms on the original page before reusing the data.
What formal language is used in CombiBench?
All problems in CombiBench are formalised using the Lean 4 interactive theorem prover.
Where do the problems come from?
The 100 problems originate from Brualdi's combinatorics textbook (42 problems), official IMO competitions since 2000 (36 problems), the Hackmath website (10 problems), and various other competitions such as APMO, Baltic Way, EGMO, IMO Shortlist, IZHO, BXMO, and USAMO (12 problems).
How are two-part problems formatted?
Problems that require providing an answer before proving its validity follow the design style of PutnamBench.
Written from CombiBench's own dataset card. Statements citing a figure that does not appear there are removed before publication. Licence and running details come from our registry.