Chocopin/MathlibPR

MathlibPR数据集基于真实的Mathlib4拉取请求历史构建，用于评估构建通过的快照的合并准备状态判断。每个快照都有一个二元的参考标签，但评估系统可以返回三种最终裁决之一：`merge_ready`、`not_merge_ready`或`uncertain`。数据集包含15,895个快照，标签分布为11,409个`merge_ready`和4,486个`not_merge_ready`。此外，还包括3,687个PR内对和六个发布的500/500代理阶段子集。该数据集旨在研究自动代码审查、形式数学工具、定理证明助手和合并准备评估等领域。

MathlibPR is built from real Mathlib4 pull request histories and evaluates merge-readiness judgments for build-passing snapshots. Each snapshot has a binary reference label, but evaluated systems may return one of three final verdicts: `merge_ready`, `not_merge_ready`, or `uncertain`. The dataset includes 15,895 snapshots with label distribution of 11,409 `merge_ready` and 4,486 `not_merge_ready`. It also includes 3,687 within-PR pairs and six released 500/500 agent-stage subsets. The dataset is intended for research on automated code review, formal mathematics tooling, theorem-proving assistants, and merge-readiness evaluation.