MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

arXiv:2605.07147v1 Announce Type: cross Abstract: The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do...