MA-ProofBench

MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis English | 中文 We introduce **MA-ProofBench**, to the best of our knowledge, the first formal benchmark for evaluating large language models (LLMs) on theorem proving in **M**athematical **A**nalysis. It contains **200** rigorously formalized theorem-proving problems in Lean 4 + Mathlib (v4.28.0), split into two difficulty tiers: | Tier | Description | Source | Count | |--------------|----------------|------------------------------------------|-------| | **Level I** | Undergraduate | Basic Textbook Exercises | 100 | | **Level II** | Ph.D. | Exam Problems from Top-Tier Universities | 100 | The problems span **6 core topics** and **27 subcategories**, including *measure and integration theory*, *complex analysis*, and *functional analysis*, among other categories. MA-ProofBench targets areas that are underrepresented in prior benchmarks and require deep reasoning about continuity, limits, and topological structures. Each problem is built through a human-led, LLM-assisted formalization pipeline with independent expert blind review to ensure mathematical fidelity. Category Distribution Problems are classified following the **Mathematics Subject Classification (MSC)** scheme: | Category | Level I | Level II | | ------------------------------- | ------- | -------- | | Real Functions | 44 | 12 | | Functional Analysis | 15 | 31 | | Functions of a Complex Variable | 19 | 16 | | Measure & Integration | 13 | 17 | | Operator Theory | 4 | 23 | | Sequences, Series, Summability | 5 | 1 | Data Fields | Field | Type | Description | | -------------------- | ------ | ------------------------------------------------------ | | `id` | int | Unique problem id within the benchmark | | `split` | string | `level1` or `level2` | | `informal_statement` | string | Natural-language statement of the problem | | `formal_statement` | string | Lean 4 theorem statement with `sorry` placeholder | | `header` | str