Dataset · Hugging Face

Pradheep1647/lean-verifier-formalizations

Name: lean-verifier-formalizations
Creator: Pradheep1647
License: mit
Keywords: task_categories:text-generation, license:mit, license:apache-2.0, license:cc-by-4.0, size_categories:n<1K, format:parquet, modality:text, library:datasets, library:pandas, library:polars, library:mlcroissant, region:us, lean4, theorem-proving, formal-verification

Lean Verifier Formalizations A dataset of Lean 4 theorem-proving tasks for evaluating agentic coding harnesses. Each row pairs a formal task_statement (with the reference proof body removed) against a real Lean 4 repository, plus the informal_excerpt/informal_source_text describing what the theorem claims, permitted_axioms for the verifier, and provenance fields (repo_url, repo_commit_sha, license) tracing back to the source project. Sources Every row is pulled… See the full description on the dataset page: https://huggingface.co/datasets/Pradheep1647/lean-verifier-formalizations.

View on Hugging FaceReport an issue

Author / organization	Pradheep1647
License (as declared)	mit
Downloads	779 (as reported by Hugging Face)
Likes	1
Created	28 August 2026
Last updated at source	14 October 2026

lean4theorem-provingformal-verificationmathlib

Embed this entry

<iframe src="https://silytics.si/embed/item/6f714350-4d24-42c2-9495-b9bfbcff42eb" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

Popularity, last 3 days

779 now (+7 since 2026-10-16). Counts as reported by the source, snapshotted daily by Silytics.

More from Pradheep1647

Pradheep1647/eagle3-speculative-decoding-energy-sweepDataset

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.