MA-ProofBench

The first formal benchmark for theorem proving in mathematical analysis: 200 Lean 4 + Mathlib problems in two tiers (100 undergraduate, 100 PhD-qualifying) across 6 topics and 27 subcategories, from Tsinghua/OpenBMB authors. Extends formal-methods evaluation beyond competition math (miniF2F, PutnamBench) into the analysis curriculum where current provers are weakest.