Dataset · Hugging Face

iiis-lean/NuminaMath-LEAN-Sol

Name: NuminaMath-LEAN-Sol
Creator: iiis-lean
License: apache-2.0
Keywords: task_categories:text-generation, language:en, license:apache-2.0, size_categories:10K<n<100K, format:json, modality:text, library:datasets, library:pandas, library:polars, library:mlcroissant, region:us, mathematics, theorem-proving, lean, formal-verification

NuminaMath-LEAN Cleaned with NL Solutions Dataset Summary This is a cleaned version of the NuminaMath-LEAN dataset, enhanced with natural language (NL) solutions matched from source datasets. The primary goal is to provide paired formal statements/proofs with natural language solutions for proof formalization and theorem proving research. The dataset matches problems from NuminaMath-LEAN with their corresponding natural language solutions from: olympiads-ref: A… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/NuminaMath-LEAN-Sol.

View on Hugging FaceReport an issue

Author / organization	iiis-lean
License (as declared)	apache-2.0
Downloads	857 (as reported by Hugging Face)
Likes	0
Created	23 January 2026
Last updated at source	23 January 2026

mathematicstheorem-provingleanformal-verificationproof-generationmath-word-problems

Embed this entry

<iframe src="https://silytics.si/embed/item/6edfc3e6-cb86-4f4a-93bb-00e38ddaff27" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

More from iiis-lean

iiis-lean/NuminaMath-LEAN-Proof-ArtifactsDataset
iiis-lean/lean-math-formal-corpusDataset

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