Omkar2118/datasets huggingface dataset:
ConstructiveBench

Enumerate–Conjecture–Prove: Formally Solving Answer-Construction Problem in Math Competitions
We release the ConstructiveBench dataset as part of our Enumerate–Conjecture–Prove (ECP) paper. It enables benchmarking automated reasoning systems on answer-construction math problems using Lean 4.

Source Repository: https://github.com/JackSun200312/ECP


Description
This dataset (constructivebench.json) contains curated Olympiad-style math problems along with metadata and aligned Lean 4 formalizations.

Each entry includes:

Problem statement
Category (e.g., Algebra, Combinatorics)
Source (e.g., IMO 2011)
Formal answer in Lean
Full formal theorem
Answer-construction alignment parts (header, answer, theorem, and theorem without answer)
Example Entry
{
  "name": "IMO2011SLC4",
  "category": "Combinatorics",
  "source": "IMO/2011",
  "problem": "...",
  "answer": "The greatest such number k is 3",
  "formalization": "...",
  "is_formalized": true,
...
}

Introducing paper: Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions