Proof Improvement Instances from Mathlib4 Code Review

123 proof-improvement instances were mined from code review on mathlib4, the Lean 4 theorem prover library. The dataset was created by SJCaldwell to benchmark language models on judging proof quality, distinct from correctness. It was last updated in March 2026.

Use Cases

• Train models to classify proof quality based on features like reviewer comments and proof changes.
• Benchmark model performance on distinguishing between proof correctness and proof style using the pull request context.
• Analyze patterns in requested proof improvements from the mined code review instances.

Strengths

• Contains 123 distinct proof-improvement instances.
• Data is sourced from real code reviews in the active mathlib4 project.

Limitations

• Small sample size of 123 instances may limit statistical power for training models.
• Scope is limited to proofs from a single library (mathlib4) in one theorem prover (Lean 4).

Provenance

Source

Code review pull requests from mathlib4, the Lean 4 mathematics library.

Collection Method

Mined from pull requests where a reviewer requested changes to one or more proofs.

Freshness

Last updated March 2026.