EPFL-LARA/lean-evaluation-benchmark

Evaluation benchmark The paper's evaluation benchmark for learned Lean 4 evaluators contains 68,932 deduplicated candidate programs from three public provers. Each row contains a complete source program and the acceptance label obtained with Lean v4.15.0. Subset Programs Valid miniF2F 41,638 25,702 (61.7%) ProofNet 27,294 2,443 (9.0%) Combined 68,932 28,145 (40.8%) The remaining 40,787 programs are invalid. Candidates come from Pythagoras-Prover-4B… See the full description on the dataset page: https://huggingface.co/datasets/EPFL-LARA/lean-evaluation-benchmark.

<iframe src="https://silytics.si/embed/item/4c7d9b98-6c33-4daa-98b2-e1d10296afb2" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 18 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.