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, ... }