LeanPolish is a dataset of Lean 4 proof rewrite pairs produced by a kernel-verified proof-shortening tool. Each accepted (original, replacement) pair was kernel-checked under Lean 4.21.0 with Mathlib v4.21.0 before emission and re-elaborated end-to-end by a separate out-of-process verifier. The dataset was authored by leanpolish-anon and last updated on May 6, 2026.
Use Cases
- Training models to compress Lean 4 proofs based on verified rewrite pairs.
- Training models to simplify Lean 4 proofs based on verified rewrite pairs.
- Benchmarking proof optimization algorithms using kernel-verified examples.
- Studying patterns in formal proof transformations.
Strengths
- All proof rewrite pairs were kernel-checked under Lean 4.21.0 with Mathlib v4.21.0.
- Rewritten files were re-elaborated end-to-end by a separate out-of-process verifier.
Limitations
- Column-level documentation is absent; field semantics must be inferred after download.
- Row count is unknown, which may limit suitability assessment.
Provenance
- Source
- huggingface
- Collection Method
- Produced by LeanPolish, a kernel-verified proof-shortening tool.
- Freshness
- Last updated 2026-05-06 19:07:12.