LeanPolish

LeanPolish is a Lean 4 proof-compression pipeline for kernel-verified proof shortening. The repository contains the verified optimizer, reproducibility scripts, and metadata for the accompanying Hugging Face dataset.

The large proof corpora and JSONL training shards are released on Hugging Face rather than stored directly in this Git repository. See leanpolish-anon/lean-proof-compression, dataset/huggingface_dataset_card.md and dataset/MANIFEST.json for schema and shard metadata.

Layout

Path	Contents
LeanPolish.lean	Main Lean executable used to enumerate, verify, and emit proof-shortening edits.
LinterBaseline.lean	Lean baseline for linter.unusedTactic comparison.
leanpolish.py, run_worker_pool.py	Python orchestration for single-file and pooled runs.
run_regression_smoke.py, regression_baseline.json	Small CI smoke test over a stratified fixed baseline.
aggregate_reports.py, audit_training_pairs.py, unify_shard_layout.py	Dataset aggregation, auditing, and shard-layout helpers.
analysis/	Scripts and frozen outputs used for tables, leakage checks, and G3 statistics.
docs/	Datasheet and reproducibility notes.
dataset/	Hugging Face dataset card and released-shard manifest.

Build

Install Lean through elan, then fetch the Mathlib cache before building:

lake exe cache get
lake build LeanPolish LinterBaseline

The repository is pinned to Lean/Mathlib v4.21.0 via lean-toolchain and lake-manifest.json. Without the Mathlib cache, a cold GitHub-hosted runner can spend more than an hour building dependencies from source.

Smoke Test

python3 run_regression_smoke.py --workers 4 --timeout 900 \
	--tolerance-pct 5 --baseline regression_baseline_ci.json

The release repository includes 12 committed smoke fixtures. The expected summary is:

=== summary: 12 pass, 0 fail, 0 error, 0 skip ===

The larger regression_baseline.json file records the 20-case smoke baseline used with a full source-corpus checkout; missing corpus files are reported as SKIP by the runner.

The same check runs in .github/workflows/smoke.yml. The workflow first runs lake exe cache get, then builds LeanPolish, then executes the smoke test and uploads smoke.log on every run.

Dataset

The released dataset consists of schema-versioned accepted proof-compression pairs and rejected contrastive siblings across Mathlib, Goedel-Workbook, miniF2F, PutnamBench-derived proof pools, and Putnam 2025 / AxiomProver sources. The Hugging Face card records the per-config JSONL layout and schema, including deduplicated headline totals.

Dataset: leanpolish-anon/lean-proof-compression.

Useful entry points:

python3 audit_training_pairs.py shards/<corpus>/training_pairs.jsonl.gz
python3 aggregate_reports.py --help
python3 unify_shard_layout.py

For exact commands, toolchain pins, and expected outputs, see docs/reproducibility.md.

Analysis

Tables, leakage checks, and G3 statistics are generated from the frozen outputs in analysis/.

License

MIT. See LICENSE.