Dataset · Hugging Face

leanpolish-anon/lean-proof-compression

Name: lean-proof-compression
Creator: leanpolish-anon
License: apache-2.0
Keywords: task_categories:text-generation, task_categories:other, task_ids:language-modeling, language:en, license:apache-2.0, size_categories:10K<n<100K, format:parquet, modality:tabular, modality:text, library:datasets, library:pandas, library:polars, library:mlcroissant, arxiv:2502.07640, arxiv:2508.03613

LeanPolish: Verified Supervision for Lean Proof Compression A dataset of Lean 4 proof rewrite pairs produced by LeanPolish, a kernel-verified proof-shortening tool. Every accepted (original, replacement) pair was kernel-checked under Lean 4.21.0 with Mathlib v4.21.0 before emission, and the rewritten file was re-elaborated end-to-end by a separate out-of-process verifier. The dataset is suitable for training models that learn to compress, simplify, or select proof tactics, and… See the full description on the dataset page: https://huggingface.co/datasets/leanpolish-anon/lean-proof-compression.

View on Hugging FaceReport an issue

Author / organization	leanpolish-anon
License (as declared)	apache-2.0
Downloads	610 (as reported by Hugging Face)
Likes	1
Created	30 April 2026
Last updated at source	26 September 2026

lean4mathlibtheorem-provingproof-optimizationverifiedrldpo

Embed this entry

<iframe src="https://silytics.si/embed/item/fd3a1b83-cd61-4fa7-8c80-9ab78b924bae" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

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.