MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis

# MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
Source: [https://arxiv.org/html/2606.13782](https://arxiv.org/html/2606.13782)
Lushi Pu1, Weiming Zhang2, Xinheng Xie1, Zixuan Fu2, Bingxiang He2, Hongya Lyu1, Xin Li1, Jie Zhou1, Yudong Wang2† 1ModelBest Inc\.2Tsinghua University pulushi@modelbest\.cnyudongwang@tsinghua\.edu\.cn

###### Abstract

Large Language Models \(LLMs\) have made notable progress in automated theorem proving, yet existing formal benchmarks remain limited in both mathematical coverage and difficulty\. Most are concentrated in areas that are easier to formalize, such as algebra and elementary number theory, and provide limited coverage of subfields that require deeper reasoning, including mathematical analysis\. To address this gap, we introduceMA\-ProofBench, to the best of our knowledge, the first formal theorem\-proving benchmark dedicated toMathematicalAnalysis\. The benchmark contains 200 formalized theorems covering 6 core topics and 27 subcategories, including measure and integration theory, complex analysis, and functional analysis\. The problems are divided into two difficulty levels, an undergraduate level \(Level I, 100 problems\) and a Ph\.D\. qualifying level \(Level II, 100 problems\), to evaluate how well LLMs perform formal reasoning at different mathematical depths\. Each problem is constructed through a human\-led, LLM\-assisted formalization pipeline followed by independent expert review, ensuring that the formal statements remain faithful to the original mathematics\. We evaluate a range of recent general\-purpose reasoning models and formal theorem provers on MA\-ProofBench\. However, most models perform poorly: even the best\-performing model, GPT\-5\.5, achieves only 16% Pass@8 on Level I and 5% on Level II, while most models stay close to 0% on Level II\. Further analysis identifies Mathlib hallucinations and incomplete proofs as the two dominant failure modes, while an evaluation on the natural\-language version of the benchmark exposes a clear gap between informal and formal reasoning\. MA\-ProofBench is intended to serve as a reliable reference for tracking progress in formal mathematical reasoning in advanced domains\.

†††\\daggerCorresponding authors\.## 1Introduction

The rapid advancement of Large Reasoning Models \(LRMs\)\(Jaechet al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib1); Guoet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib2)\)has driven significant progress in end\-to\-end automated theorem proving\. As natural language proofs become increasingly long and intricate, manual verification by human experts has emerged as a major bottleneck for AI\-assisted mathematics\. Formal verification via interactive theorem provers such as Lean 4\(Moura and Ullrich,[2021](https://arxiv.org/html/2606.13782#bib.bib3)\)offers a scalable and reliable alternative\. Building on this approach, recent models\(Linet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib18); Renet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib17); Chenet al\.,[2025b](https://arxiv.org/html/2606.13782#bib.bib19)\)have demonstrated the ability to generate non\-trivial formal proofs across diverse benchmarks, including challenging problems from the International Mathematical Olympiad \(IMO\)\.

Despite this progress, existing formal benchmarks fall short of providing a comprehensive assessment of model capabilities in complex mathematical reasoning\. The discriminative power of some traditional benchmarks is diminishing; for instance, Seed\-Prover\(Chenet al\.,[2025b](https://arxiv.org/html/2606.13782#bib.bib19)\)has effectively saturated miniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2606.13782#bib.bib10)\), achieving a 100% success rate\. Moreover, the quality of the formal statements directly affects the reliability of evaluation\. Recent studies\(Ammanamanchi and Bhat,[2025](https://arxiv.org/html/2606.13782#bib.bib5); Ospanovet al\.,[2026](https://arxiv.org/html/2606.13782#bib.bib4)\)have shown that some existing datasets contain semantic flaws, imprecise statements, or formalizations that do not fully match the intended mathematical meaning of the original problems\. More importantly, current benchmarks, such as FIMO\(Liuet al\.,[2023](https://arxiv.org/html/2606.13782#bib.bib6)\), Putnam\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib7)\), ProofNet\(Azerbayevet al\.,[2023](https://arxiv.org/html/2606.13782#bib.bib8)\), and FormalMATH\(Yuet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib9)\), exhibit an uneven topic distribution\. Many problems are concentrated in areas that are comparatively easier to formalize, such as algebra, elementary number theory, combinatorics, or discrete structures, while fields that require reasoning jointly about continuity, limits, and topological structures, such as measure theory, complex analysis, and functional analysis, remain underrepresented\.

Mathematical Analysis \(MA\) is a central branch of modern mathematics, studying continuity, limits, and infinite processes\. Theorem proving in this domain is often demanding, as it requires both an understanding of the key structures involved and the ability to decompose a goal into a sequence of verifiable intermediate steps, making it a particularly challenging target for current formal systems\. To address the limited coverage of analysis in existing formal benchmarks, we introduceMA\-ProofBench, a high\-quality, broad\-coverage, two\-tiered formal benchmark dedicated to mathematical analysis\.

The problems in MA\-ProofBench are mainly collected from widely used undergraduate analysis textbooks and publicly available Ph\.D\. qualifying exams, yielding two difficulty levels:*Level I*contains foundational exercises from the standard undergraduate curriculum, while*Level II*comprises more sophisticated analysis problems from doctoral qualifying examinations\. To ensure the mathematical fidelity of the formal statements, we employ a human\-led, LLM\-assisted formalization pipeline coupled with a rigorous independent expert review stage\. The resulting dataset provides a robust framework for evaluating the formal reasoning capabilities of models in mathematical analysis\.

We evaluate both general\-purpose reasoning models and formal theorem provers on MA\-ProofBench\. The evaluation reveals that both general\-purpose reasoning models and formal theorem provers struggle with MA\-ProofBench: the best\-performing general\-purpose reasoning model, GPT\-5\.5, achieves only 16% Pass@8 on Level I and 5% on Level II, while the strongest theorem prover, DeepSeek\-Prover\-V2\-671B, reaches just 6\.86% and 0\.44%, respectively\. These results show that current models still struggle with formal proofs in advanced analysis\. Further analysis attributes the majority of failures to Mathlib hallucinations and incomplete proofs, while an evaluation on the natural\-language version of the benchmark exposes a clear gap between informal and formal reasoning\.

Our main contributions are summarized as follows:

- •We introduceMA\-ProofBench, the first formal benchmark dedicated to mathematical analysis\. It comprises two difficulty levels \(undergraduate and Ph\.D\.\), each with 100 problems, covering 6 core topics and 27 subcategories\.
- •We propose a human\-led, LLM\-assisted formalization workflow that addresses the semantic and syntactic challenges of translating advanced analysis problems into Lean 4, thereby ensuring the quality of the resulting formal statements\.
- •We evaluate a broad range of general\-purpose reasoning models and formal theorem provers on MA\-ProofBench\. The results identify Mathlib hallucinations and incomplete proofs as the dominant failure modes, and further reveal a substantial gap between models’ informal and formal reasoning abilities\.

## 2Related Works

### 2\.1Formal Theorem Proving

The field of automated theorem proving is evolving from single\-paradigm search toward more sophisticated search\-augmented and agent\-based methods\. Since OpenAI’s GPT\-f\(Polu and Sutskever,[2020](https://arxiv.org/html/2606.13782#bib.bib11)\)adopted best\-first search and DeepMind’s AlphaProof\(Hubertet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib12)\)achieved strong results on IMO\-style problems, the open\-source community has explored several technical directions\. Tree\-search\-based methods such as InternLM2\.5\-StepProver\(Wuet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib13)\), BFS\-Prover\(Xinet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib14)\), DeepSeek\-Prover\-V1\.5\(Xinet al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib48)\), and HunyuanProver\(Liet al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib15)\)explore tactic\-level tree search algorithms such as Monte Carlo Tree Search\. In contrast, whole\-proof generation methods such as Kimina\-Prover\(Wanget al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib16)\), DeepSeek\-Prover\-V2\(Renet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib17)\), and Goedel\-Prover\(Linet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib18)\)generate the entire proof in a single pass\. Another line of work augments formal proof search and verification by building agent\-based systems, including Seed\-Prover\(Chenet al\.,[2025b](https://arxiv.org/html/2606.13782#bib.bib19),[a](https://arxiv.org/html/2606.13782#bib.bib20)\), Aristotle\(Achimet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib21)\), Ax\-Prover\(Breenet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib47)\), and Numina\-Lean\-Agent\(Liuet al\.,[2026](https://arxiv.org/html/2606.13782#bib.bib22)\)\.

### 2\.2Mathematical Benchmarks

Existing mathematical benchmarks can be broadly categorized as informal or formal\. Informal benchmarks including GSM8K\(Cobbeet al\.,[2021](https://arxiv.org/html/2606.13782#bib.bib23)\), MATH\(Hendryckset al\.,[2021](https://arxiv.org/html/2606.13782#bib.bib24)\), AIME\([MAA,](https://arxiv.org/html/2606.13782#bib.bib39)\), OlympiadBench\(Heet al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib25)\), Omni\-MATH\(Gaoet al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib38)\), IMO\-AnswerBench\(Luonget al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib26)\), and AMO\-Bench\(Anet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib27)\)focus mainly on numerical problem solving with final\-answer evaluation, while IMO\-ProofBench\(Luonget al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib26)\)and ProofBench\(Maet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib28)\)evaluate natural language proof generation\. In formal mathematics, early benchmarks such as miniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2606.13782#bib.bib10)\)and FIMO\(Liuet al\.,[2023](https://arxiv.org/html/2606.13782#bib.bib6)\)primarily cover competition\-level problems, ranging from high school competitions to the IMO\. Subsequent benchmarks such as ProofNet\(Azerbayevet al\.,[2023](https://arxiv.org/html/2606.13782#bib.bib8)\), PutnamBench\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2606.13782#bib.bib7)\), and FormalMATH\(Yuet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib9)\)expand the scope to the undergraduate level, but their content remains concentrated in areas such as algebra, topology, and elementary calculus\. Recent benchmarks also target specific domains, such as CombiBench\(Liuet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib29)\), FATE\(Jianget al\.,[2026](https://arxiv.org/html/2606.13782#bib.bib30)\), and LeanCat\(Xuet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib31)\)\. MA\-ProofBench follows this domain\-specific line of work and focuses on mathematical analysis, a subfield that remains underrepresented in existing formal benchmarks\.

## 3MA\-ProofBench Construction and Characteristics

### 3\.1Benchmark Overview

Table 1:Difficulty Level DistributionLevelDescriptionSourceCountLevel IUndergraduateBasic Textbook Exercises100Level IIPh\.D\.Exam Problems From Top\-Tier Universities100![Refer to caption](https://arxiv.org/html/2606.13782v1/x1.png)\(a\)Category distribution for Level I
![Refer to caption](https://arxiv.org/html/2606.13782v1/x2.png)\(b\)Category distribution for Level II

Figure 1:Category distribution of MA\-ProofBench across Level I and Level II problems\. The inner ring represents high\-level mathematical topics, while the outer ring shows their finer\-grained subcategories\. For readability, only subcategories with relatively high frequency are annotated in the outer ring, although all subcategories are included in the proportional areas\. A detailed breakdown of the category distribution is provided in Appendix[A](https://arxiv.org/html/2606.13782#A1)\.The problems in MA\-ProofBench are collected primarily from widely used undergraduate textbooks in mathematical analysis and publicly accessible Ph\.D\. qualifying examination papers\. Specifically, the problems are organized according to the Mathematics Subject Classification \(MSC\), encompassing 6 core categories of analysis: Real Functions, Measure and Integration, Functions of a Complex Variable, Sequences, Series, and Summability, Functional Analysis, and Operator Theory\. These are further subdivided into 27 subcategories, with the detailed distribution illustrated in Table[1](https://arxiv.org/html/2606.13782#S3.T1)and Figure[1](https://arxiv.org/html/2606.13782#S3.F1)\.

In terms of topic distribution, Level I primarily focuses on foundational topics in analysis, such as functions of one variable and classical measure theory\. In contrast, Level II emphasizes deeper abstract structures, with a strong focus on advanced topics such as linear function spaces in functional analysis, the general theory of linear operators, advanced measure theory, and geometric function theory\. Figure[2](https://arxiv.org/html/2606.13782#S3.F2)shows representative examples for each level\.

Example of Level IQuestion:Supposef∈L1​\(μ\)f\\in L^\{1\}\(\\mu\)\. Prove that for eachϵ\>0\\epsilon\>0there exists aδ\>0\\delta\>0such that∫E\|f\|​𝑑μ<ϵ\\int\_\{E\}\|f\|\\,d\\mu<\\epsilonwheneverμ​\(E\)<δ\\mu\(E\)<\\delta\.Formal Statement: [⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCm9wZW4gTWVhc3VyZVRoZW9yeQoKdGhlb3JlbSBtYV9wcm9vZmJlbmNoX2wxXzg1IHvOsSA6IFR5cGUqfSBbTWVhc3VyYWJsZVNwYWNlIM6xXSB7zrwgOiBNZWFzdXJlIM6xfSB7ZiA6IM6xIOKGkiDihJ19CiAgICAoaGYgOiBJbnRlZ3JhYmxlIGYgzrwpIDoKICAgIOKIgCDOtSA6IOKEnSwgMCA8IM61IOKGkiDiiIMgzrQgOiBFTk5SZWFsLCAwIDwgzrQg4oinCiAgICAgIOKIgCBFIDogU2V0IM6xLCBNZWFzdXJhYmxlU2V0IEUg4oaSIM68IEUgPCDOtCDihpIgKOKIqyB4IGluIEUsIOKAlmYgeOKAliDiiILOvCkgPCDOtSA6PSBieQogIHNvcnJ5)import𝒩\\mathcal\{N\}Mathlibopen𝒩\\mathcal\{N\}MeasureTheorytheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_85𝒩\\mathcal\{N\}\{α\\alpha𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Type\*\}𝒩\\mathcal\{N\}\[MeasurableSpace𝒩\\mathcal\{N\}α\\alpha\]𝒩\\mathcal\{N\}\{μ\\mu𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Measure𝒩\\mathcal\{N\}α\\alpha\}𝒩\\mathcal\{N\}\{f𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}α\\alpha𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(hf𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Integrable𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}μ\\mu\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}ε\\varepsilon𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\},𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}ε\\varepsilon𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}δ\\delta𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ENNReal,𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}δ\\delta𝒩\\mathcal\{N\}∧\\wedge𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}E𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}α\\alpha,𝒩\\mathcal\{N\}MeasurableSet𝒩\\mathcal\{N\}E𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}μ\\mu𝒩\\mathcal\{N\}E𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}δ\\delta𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}\(∫\\int𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}in𝒩\\mathcal\{N\}E,𝒩\\mathcal\{N\}∥\\\|f𝒩\\mathcal\{N\}x∥\\\|𝒩\\mathcal\{N\}∂\\partialμ\\mu\)𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}ε\\varepsilon𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}sorry

Example of Level IIQuestion:LetXXbe a reflexive complex Banach space,C⊂XC\\subset Xbe a closed convex subset, show that for allx0∈Xx\_\{0\}\\in X, there existsy0∈Cy\_\{0\}\\in Csuch that‖x0−y0‖=infy∈C‖x0−y‖\.\\\|x\_\{0\}\-y\_\{0\}\\\|=\\inf\_\{y\\in C\}\\\|x\_\{0\}\-y\\\|\.Formal Statement: [⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMl82NAogIChYIDogVHlwZSopIFtOb3JtZWRBZGRDb21tR3JvdXAgWF0gW05vcm1lZFNwYWNlIOKEgiBYXSBbQ29tcGxldGVTcGFjZSBYXQogIChoWF9yZWZsZXhpdmUgOiBGdW5jdGlvbi5TdXJqZWN0aXZlIChOb3JtZWRTcGFjZS5pbmNsdXNpb25JbkRvdWJsZUR1YWwg4oSCIFgpKSAoQyA6IFNldCBYKQogIChoQ19jbG9zZWQgOiBJc0Nsb3NlZCBDKSAoX2hDX2NvbnZleCA6IENvbnZleCDihJ0gQykgKGhDX25vbmVtcHR5IDogQy5Ob25lbXB0eSkgOgogIOKIgCB44oKAIDogWCwg4oiDIHnigoAg4oiIIEMsIOKAlnjigoAgLSB54oKA4oCWID0g4qiFIHkgOiBDLCDigJZ44oKAIC0gKHkgOiBYKeKAliA6PSBieQogIHNvcnJ5)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l2\_64𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(X𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Type\*\)𝒩\\mathcal\{N\}\[NormedAddCommGroup𝒩\\mathcal\{N\}X\]𝒩\\mathcal\{N\}\[NormedSpace𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}X\]𝒩\\mathcal\{N\}\[CompleteSpace𝒩\\mathcal\{N\}X\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(hX\_reflexive𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Function\.Surjective𝒩\\mathcal\{N\}\(NormedSpace\.inclusionInDoubleDual𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}X\)\)𝒩\\mathcal\{N\}\(C𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}X\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(hC\_closed𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}IsClosed𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}\(\_hC\_convex𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Convex𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}\(hC\_nonempty𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}C\.Nonempty\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}x0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}X,𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}y0𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}C,𝒩\\mathcal\{N\}∥\\\|x0𝒩\\mathcal\{N\}\-𝒩\\mathcal\{N\}y0∥\\\|𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}⨅\\bigsqcap𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}C,𝒩\\mathcal\{N\}∥\\\|x0𝒩\\mathcal\{N\}\-𝒩\\mathcal\{N\}\(y𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}X\)∥\\\|𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}sorry

Figure 2:Comparison of problem difficulty\. The Level I example involves a basic absolute continuity theorem in measure theory with straightforward typing\. In contrast, the Level II example requires setting up heavy mathematical machinery, such as reflexive Banach spaces and double duals, illustrating the increased conceptual and syntactic complexity\.
### 3\.2Curation Workflow

We constructed the benchmark through a four\-stage workflow driven by human\-LLM collaboration, as illustrated in Figure[3](https://arxiv.org/html/2606.13782#S3.F3):

1. 1\.Problem Collection:We collected raw problems and conducted several rounds of cleaning and proofreading to correct inaccurate statements, standardize the mathematical content, and unify the formatting, removing ambiguous or incomplete entries along the way\. This yielded a candidate pool of about 500 problems, from which we selected a representative subset of 200 problems\.
2. 2\.Formalization:Human experts first translated each natural\-language problem into a draft Lean 4 statement, leaving the proof assorry\. They then iterated in a “formalize–feedback–refine” loop, using Lean 4 compiler messages \(e\.g\., type mismatches or unknown identifiers\) to fix the code and add missing imports\. For unfamiliar Mathlib APIs, experts consulted LLM suggestions and cross\-checked them against the official Mathlib documentation\. Final decisions were always made by the human experts, ensuring that the formal statements remained faithful to the original problems\.
3. 3\.Independent Expert Review:Each formal statement was then independently reviewed by three additional experts\. Each reviewer was required to “reverse\-translate” the Lean 4 code back into its intended mathematical statement, ensuring that no implicit assumption was dropped and no condition was inadvertently weakened\. A theorem was accepted only if at least two reviewers voted in favor; otherwise, it was sent back to Stage 2 for revision\.
4. 4\.Difficulty Grading:Based on the intrinsic mathematical complexity and the difficulty of formalization, experts scored and categorized the problems into Level I and Level II\. The evaluation criteria include: - •The number of critical sub\-tasks or lemmas required for the proof\. - •The level of conceptual abstraction \(e\.g\., elementary limit calculations versus the construction of abstract measure spaces\)\.

![Refer to caption](https://arxiv.org/html/2606.13782v1/x3.png)Figure 3:Overview of the curation workflow of MA\-ProofBench, comprising Problem Collection, Formalization, Independent Expert Review, and Difficulty Grading\.
### 3\.3Formalization Standards

To ensure the semantic fidelity of each formal statement to its informal counterpart, MA\-ProofBench adheres to a unified set of formalization conventions:

Function Definitions\.In informal mathematics, a function is sometimes defined only on a certain subset\. In formalization, however, we typically represent it as a total function on the ambient space and make the actual domain of interest explicit through a predicate or a set condition\. This treatment keeps the function type uniform and avoids frequent coercions between subtypes and the ambient space, thereby allowing us to directly reuse Mathlib’s general definitions and theorems for notions such as continuity, differentiability, and harmonicity\. In this setting, the values outside the specified subset do not carry mathematical content; the relevant statements are asserted only on the prescribed set or in its neighborhood\.

Integration Framework\.For integrals in natural\-language problem statements whose values lie in a normed linear space, in particular for real\- or complex\-valued integrals, we formalize them as Bochner integrals in Lean\. This convention applies only when the target space carries the relevant normed linear structure; for objects such as extended nonnegative real\-valued integrals, we still use Mathlib’s dedicated framework for nonnegative Lebesgue integration\.

Spatial Structures\.Natural\-language problem statements sometimes leave implicit the distinction betweenLpL^\{p\}equivalence classes and pointwise\-defined functions, whereas formalization requires this distinction to be made explicit\. We therefore choose the representation according to the mathematical structure on which each statement depends\. For properties intrinsic toLpL^\{p\}spaces, such as norms, distances, convergence, and bounded linear operators, functions are formalized as equivalence classes modulo almost\-everywhere equality, which preserves the standard normed space structure ofLpL^\{p\}\. For statements involving values at specific points, pointwise inequalities, or pointwise regularity, we instead work with concrete function representatives\.

Explicit Premises\.Implicit mathematical assumptions are stated explicitly in the formal theorem\. Because Lean quantifies over every object satisfying the declared premises, non\-degeneracy assumptions that are commonly left tacit in informal writing, such as nonemptiness captured by\[Nonempty X\], are added directly to the statement\. Doing so prevents the formal theorem from being trivially or vacuously satisfied in boundary or degenerate cases, and keeps its semantic scope aligned with that of the original problem\.

## 4Experiments

### 4\.1Experimental Setting

We evaluated a range of models on MA\-ProofBench, including formal theorem provers \(DeepSeek\-Prover\-V2 \(7B and 671B\)\(Renet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib17)\), Kimina\-Prover\-72B\(Wanget al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib16)\), and Goedel\-Prover\-V2 \(8B and 32B\)\(Linet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib18)\)\); open\-source general\-purpose reasoning models, including DeepSeek\-V3\.2\-Thinking\(DeepSeek\-AIet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib34)\), GLM\-5\.1\(Z\.ai,[2026](https://arxiv.org/html/2606.13782#bib.bib43)\), Qwen3\.5\-397B\-A17B\(Qwen Team,[2026](https://arxiv.org/html/2606.13782#bib.bib35)\), Qwen3\-235B\-Thinking\-2507\(Team,[2025](https://arxiv.org/html/2606.13782#bib.bib36)\), Nemotron\-3\-Nano\-30B\-A3B\(NVIDIA,[2025](https://arxiv.org/html/2606.13782#bib.bib37)\), and GPT\-OSS\-120B \(High\)\(OpenAI,[2025](https://arxiv.org/html/2606.13782#bib.bib44)\); and proprietary models, namely GPT\-5\.5 \(xhigh\)\(OpenAI,[2026](https://arxiv.org/html/2606.13782#bib.bib42)\), Gemini 3\.1 Pro \(High\)\(Google DeepMind,[2026](https://arxiv.org/html/2606.13782#bib.bib40)\), and Claude Sonnet 4\.6 \(High\)\(Anthropic,[2026](https://arxiv.org/html/2606.13782#bib.bib41)\)\. The generation parameters were configured with a maximum output length of 32k tokens and a temperature of 1\.0\. For evaluation, we used the Pass@kkmetric\(Chenet al\.,[2021](https://arxiv.org/html/2606.13782#bib.bib33)\), which is formally defined as follows:

Pass​@​k=1N​∑i=1N\(1−\(n−cik\)\(nk\)\),\\text\{Pass\}@k=\\frac\{1\}\{N\}\\sum\_\{i=1\}^\{N\}\\left\(1\-\\frac\{\\binom\{n\-c\_\{i\}\}\{k\}\}\{\\binom\{n\}\{k\}\}\\right\),whereNNis the total number of problems in the benchmark,nndenotes the number of candidate proofs generated per problem, andcic\_\{i\}denotes the number of successful proofs among thenncandidates for theii\-th problem\.

For all open\-source models, we generatedn=32n=32candidate proofs per problem, while for the proprietary GPT\-5\.5 \(xhigh\), Gemini 3\.1 Pro \(High\), and Claude Sonnet 4\.6 \(High\), we usedn=8n=8due to API budget constraints\. We therefore adopt Pass@8 as the primary metric for cross\-model comparison, and report Pass@32 only as a supplementary result for the models sampled withn=32n=32\. All evaluations were run on Mathlib 4\.28\.0\(mathlib Community,[2020](https://arxiv.org/html/2606.13782#bib.bib45)\), with Kimina Lean Server\(Santoset al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib32)\)as the compilation backend for its efficiency\. We establish the following criteria for a proof to be considered successful:

- •The proof must pass compiler verification without generating any errors\.
- •The proof must not contain anysorryplaceholders\.
- •The proof must include all prerequisite components \(e\.g\., definitions\) required by the original problem, while leaving the theorem statement itself strictly unaltered\.

The exact prompts used in our evaluation are provided in Appendix[C](https://arxiv.org/html/2606.13782#A3)\.

### 4\.2Main Results

Table 2:Performance evaluation of different models on MA\-ProofBench\. Accuracies \(%\) are reported under Pass@1, Pass@8, and Pass@32 settings\. Pass@8 is used as the primary cross\-model comparison; Pass@32 is reported only for the models sampled withn=32n=32\.ModelLevel ILevel IIPass@1Pass@8Pass@32Pass@1Pass@8Pass@32Closed\-Source Reasoning ModelsGPT\-5\.5 \(xhigh\)6\.5016\.00–1\.755\.00–Gemini 3\.1 Pro \(High\)4\.3813\.00–1\.635\.00–Claude Sonnet 4\.6 \(High\)3\.506\.00–0\.503\.00–Open\-Source Reasoning ModelsDeepSeek\-V3\.2\-Thinking2\.095\.567\.000\.661\.852\.00GLM\-5\.10\.060\.441\.000\.000\.000\.00Qwen3\.5\-397B\-A17B0\.873\.145\.000\.000\.000\.00Qwen3\-235B\-Thinking\-25070\.030\.251\.000\.000\.000\.00Nemotron\-3\-Nano\-30B\-A3B2\.123\.594\.000\.000\.000\.00GPT\-OSS\-120B \(High\)0\.060\.502\.000\.000\.000\.00Theorem ProversDeepSeek\-Prover\-V2\-671B3\.226\.869\.000\.060\.441\.00Kimina\-Prover\-72B1\.123\.114\.000\.000\.000\.00Goedel\-Prover\-V2\-32B2\.845\.056\.000\.000\.000\.00Goedel\-Prover\-V2\-8B1\.973\.845\.000\.000\.000\.00DeepSeek\-Prover\-V2\-7B0\.943\.466\.000\.000\.000\.00Table[2](https://arxiv.org/html/2606.13782#S4.T2)summarizes the main evaluation results, from which we highlight three observations\.

- •Closed\-source reasoning models lead overall\.GPT\-5\.5 \(xhigh\) attains the highest Pass@8 on Level I \(16%\) and ties Gemini 3\.1 Pro \(High\) for the best Pass@8 on Level II \(5%\)\.
- •Formal theorem provers remain strong on Level I\.DeepSeek\-Prover\-V2\-671B reaches 6\.86% Pass@8 and 9% Pass@32 on Level I, outperforming all open\-source general\-purpose reasoning models on this split\. A separate observation is that, despite having only∼\\sim3B active parameters, Nemotron\-3\-Nano\-30B\-A3B reaches 2\.12% Pass@1 and 3\.59% Pass@8 on Level I, clearly above several open\-source reasoning models of similar or larger scale\. Given that its post\-training stage incorporates large\-scale Lean 4 formal\-proof SFT examples, this result suggests that formal\-proof data may help smaller models acquire direct proof\-generation ability\. On Level II, however, formal theorem provers reach at most 1% Pass@32 and no longer outperform the best open\-source general\-purpose reasoning model, DeepSeek\-V3\.2\-Thinking, which reaches 2%\. This indicates that the theorem prover advantage observed on Level I does not carry over to problems requiring deeper analytical reasoning\.
- •Level II exposes a substantial capability gap\.All model families perform much worse on Level II, and even the strongest models solve only a small fraction of the problems\. This suggests that this split stresses capabilities beyond local tactic selection or short proof completion, including long\-range proof planning, the construction of domain\-specific auxiliary lemmas, and reliable use of deeper Mathlib knowledge in mathematical analysis\.

## 5Further Analysis

### 5\.1Error Classification in Formal Proofs

![Refer to caption](https://arxiv.org/html/2606.13782v1/x4.png)\(a\)Error category distribution on Level I
![Refer to caption](https://arxiv.org/html/2606.13782v1/x5.png)\(b\)Error category distribution on Level II

Figure 4:Distribution of error categories across representative models on MA\-ProofBench\. The figure reports the number of failed proof attempts assigned to each error type, including Mathlib hallucination, type system error, incomplete proof, and Lean syntax error\.To better understand why models fail, we perform an error attribution analysis based on Lean compiler feedback and manual inspection, and summarize the failed proofs into four major error types\.

Mathlib Hallucinations\.These errors stem from the model referencing fictitious or mismatched Mathlib definitions, theorems, and identifiers, which triggerUnknown ConstantorUnknown Identifiercompiler errors\. Two common cases arenamespace omission, where the referenced theorem exists in Mathlib but the model fails toopenthe corresponding namespace, andname fabrication, where the model “guesses” and fabricates non\-existent theorem names based on Mathlib’s naming conventions in an attempt to complete the proof\.

Type System Errors\.The type of an expression does not match the type expected in context\. In analysis, the most common case is confusingℝ\\mathbb\{R\}withENNReal\(extended non\-negative reals\), which suggests that the model does not clearly separate metric values from measure values\. This category also covers mismatched function signatures and typeclass synthesis failures, where the model cannot supply the structures required for the proof \(e\.g\.,MetricSpaceorMeasurableSpace\)\.

Incomplete Proofs\.These proofs contain unresolved sub\-goals orsorryplaceholders\. Typical patterns includetactic misuse, where the model employs general\-purpose tactics for tasks beyond their capabilities, such as usinglinarithfor complex non\-linear inequalities or expectingsimpto automate deep analytical reasoning, andexplicit sorry insertion, where the model deliberately insertssorryto bypass substantial logical leaps or complex sub\-proofs\.

Lean Syntax Errors\.This category refers to code that violates Lean 4 syntax rules, causing the parser to fail\. Typical phenomena includemode confusion, where the model fails to distinguish the syntactic boundaries between Term Mode and Tactic Mode, andillegal identifiers, such as the misuse of reserved words or special symbols \(e\.g\., usingλ\\lambdain inappropriate contexts\), or code structures that do not conform to the Lean 4 macro system specifications\.

Furthermore, we conducted a random sampling of the failure cases produced by DeepSeek\-Prover\-V2\-671B, DeepSeek\-V3\.2\-Thinking, and Gemini 3\.1 Pro across both Level I and Level II problems, with the resulting error distribution summarized in Figure[4](https://arxiv.org/html/2606.13782#S5.F4)\. Overall, Mathlib hallucinations and incomplete proofs constitute the primary sources of error\. This trend is particularly pronounced for DeepSeek\-Prover\-V2\-671B and DeepSeek\-V3\.2\-Thinking, which yielded 80 and 82 such instances in Level I, and 78 and 62 instances in Level II, respectively\. Gemini 3\.1 Pro shows a different pattern on Level II: its dominant failure mode is incomplete proofs \(80 instances\), much higher than the other models, suggesting that it tends to leave proofs unfinished on harder problems\. Type system errors occur at a fairly stable rate across models and difficulty levels\. Although Lean syntax errors are the least frequent overall, DeepSeek\-V3\.2\-Thinking has more of these errors on Level II \(37 instances\), suggesting lower syntactic stability on harder problems\.

### 5\.2Gap Between Informal and Formal Reasoning

An inspection of the reasoning traces shows that, on most problems, the models follow a two\-stage strategy: an informal proof is first developed within the chain\-of\-thought, and only then translated into Lean 4 code\. Under this pipeline, our main results reveal a phenomenon worth highlighting: several open\-source models with otherwise strong general reasoning ability, such as GLM\-5\.1 and Qwen3\-235B\-Thinking\-2507, score close to zero in the formal setting\. A natural question is whether this gap originates from a deficiency in the underlying mathematical reasoning, or from the difficulty of converting an informal proof into Lean 4\.

Table 3:Number of fully correct Pass@1 informal proofs per level, as judged by GPT\-5\.5\.ModelLevel ILevel IIQwen3\-235B\-Thinking\-25076642DeepSeek\-V3\.2\-Thinking8566GLM\-5\.19075To address this question, we evaluate the same models on the natural\-language version of MA\-ProofBench\. Each model produces a single informal proof per problem under Pass@1, which is then graded by GPT\-5\.5 on a three\-level scale \(0, 0\.5, or 1\) following the protocol of DeepSeekMath\-V2\(Shaoet al\.,[2025](https://arxiv.org/html/2606.13782#bib.bib49)\)\. Table[3](https://arxiv.org/html/2606.13782#S5.T3)reports the number of fully correct proofs that received a score of 1, the judging prompt is given in Appendix[C](https://arxiv.org/html/2606.13782#A3)\.

Juxtaposing these results with the formal evaluation in Table[2](https://arxiv.org/html/2606.13782#S4.T2)reveals a clear gap between informal and formal reasoning: GLM\-5\.1 produces 90 and 75 fully correct informal proofs across the two levels, while its Pass@32 in the formal setting remains close to zero, and the same pattern is observed for Qwen3\-235B\-Thinking\-2507\. For these models, the bottleneck lies in faithfully expressing such reasoning as Lean 4 code that the compiler accepts\.

At the same time, formal performance is not fully determined by informal proficiency\. DeepSeek\-V3\.2\-Thinking scores below GLM\-5\.1 on the informal task, yet remains the strongest open\-source general\-purpose reasoning model in the formal setting, indicating that familiarity with Mathlib, handling of the type system, and the ability to discharge remaining subgoals all contribute substantially to the final formal score\.

## 6Conclusion

In this paper, we introduceMA\-ProofBench, a formal theorem\-proving benchmark dedicated to mathematical analysis, comprising 200 theorems across two difficulty levels \(Level I and Level II\)\. Our human\-led, LLM\-assisted formalization pipeline, combined with independent expert review, ensures broad coverage of analytical subfields, high\-quality formal statements, and substantial difficulty for current systems\. Both general\-purpose reasoning models and formal theorem provers struggle with MA\-ProofBench, with Mathlib hallucinations and incomplete proofs as the main bottlenecks, while an evaluation on the natural\-language version of the benchmark further exposes a substantial translation gap between informal reasoning and verifiable Lean 4 proofs\. These findings suggest that future systems will require better grounding in Mathlib, stronger proof\-completion capabilities for analysis\-heavy Lean proofs, and more reliable translation from informal proofs into compilable Lean 4 code\. We hope MA\-ProofBench will serve as a rigorous testbed for advancing formal reasoning in advanced mathematics\.

## References

- T\. Achim, A\. Best, A\. Bietti, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leistner, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg,et al\.\(2025\)Aristotle: imo\-level automated theorem proving\.arXiv preprint arXiv:2510\.01346\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- Faults in our formal benchmarks\.InThe 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025,External Links:[Link](https://openreview.net/forum?id=gJ2CpndJmI)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1)\.
- S\. An, X\. Cai, X\. Cao, X\. Li, Y\. Lin, J\. Liu, X\. Lv, D\. Ma, X\. Wang, Z\. Wang, and S\. Zhou \(2025\)AMO\-bench: large language models still struggle in high school math competitions\.External Links:2510\.26768,[Link](https://arxiv.org/abs/2510.26768)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- Anthropic \(2026\)Introducing Claude Sonnet 4\.6\.Note:[https://www\.anthropic\.com/news/claude\-sonnet\-4\-6](https://www.anthropic.com/news/claude-sonnet-4-6)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. Avigad \(2023\)ProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.External Links:2302\.12433,[Link](https://arxiv.org/abs/2302.12433)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- B\. Breen, M\. D\. Tredici, J\. McCarran, J\. A\. Mijares, W\. W\. Yin, K\. Sulimany, J\. M\. Taylor, F\. H\. L\. Koppens, and D\. Englund \(2025\)Ax\-prover: a deep reasoning agentic framework for theorem proving in mathematics and quantum physics\.External Links:2510\.12787,[Link](https://arxiv.org/abs/2510.12787)Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- J\. Chen, W\. Chen, J\. Du, J\. Hu, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, W\. Shi,et al\.\(2025a\)Seed\-prover 1\.5: mastering undergraduate\-level theorem proving via learning from experience\.arXiv preprint arXiv:2512\.17260\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- L\. Chen, J\. Gu, L\. Huang, W\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma,et al\.\(2025b\)Seed\-prover: deep and broad reasoning for automated theorem proving\.arXiv preprint arXiv:2507\.23726\.Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1),[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. de Oliveira Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman, A\. Ray, R\. Puri, G\. Krueger, M\. Petrov, H\. Khlaaf, G\. Sastry, P\. Mishkin, B\. Chan, S\. Gray, N\. Ryder, M\. Pavlov, A\. Power, L\. Kaiser, M\. Bavarian, C\. Winter, P\. Tillet, F\. P\. Such, D\. Cummings, M\. Plappert, F\. Chantzis, E\. Barnes, A\. Herbert\-Voss, W\. H\. Guss, A\. Nichol, A\. Paino, N\. Tezak, J\. Tang, I\. Babuschkin, S\. Balaji, S\. Jain, W\. Saunders, C\. Hesse, A\. N\. Carr, J\. Leike, J\. Achiam, V\. Misra, E\. Morikawa, A\. Radford, M\. Knight, M\. Brundage, M\. Murati, K\. Mayer, P\. Welinder, B\. McGrew, D\. Amodei, S\. McCandlish, I\. Sutskever, and W\. Zaremba \(2021\)Evaluating large language models trained on code\.External Links:2107\.03374,[Link](https://arxiv.org/abs/2107.03374)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. Schulman \(2021\)Training verifiers to solve math word problems\.External Links:2110\.14168,[Link](https://arxiv.org/abs/2110.14168)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- DeepSeek\-AI, A\. Liu, A\. Mei, B\. Lin, B\. Xue, B\. Wang, B\. Xu, B\. Wu, B\. Zhang, C\. Lin, C\. Dong, C\. Lu, C\. Zhao, C\. Deng, C\. Xu, C\. Ruan, D\. Dai, D\. Guo, D\. Yang, D\. Chen, E\. Li, F\. Zhou, F\. Lin, F\. Dai, G\. Hao, G\. Chen, G\. Li, H\. Zhang, H\. Xu, H\. Li, H\. Liang, H\. Wei, H\. Zhang, H\. Luo, H\. Ji, H\. Ding, H\. Tang, H\. Cao, H\. Gao, H\. Qu, H\. Zeng, J\. Huang, J\. Li, J\. Xu, J\. Hu, J\. Chen, J\. Xiang, J\. Yuan, J\. Cheng, J\. Zhu, J\. Ran, J\. Jiang, J\. Qiu, J\. Li, J\. Song, K\. Dong, K\. Gao, K\. Guan, K\. Huang, K\. Zhou, K\. Huang, K\. Yu, L\. Wang, L\. Zhang, L\. Wang, L\. Zhao, L\. Yin, L\. Guo, L\. Luo, L\. Ma, L\. Wang, L\. Zhang, M\. S\. Di, M\. Y\. Xu, M\. Zhang, M\. Zhang, M\. Tang, M\. Zhou, P\. Huang, P\. Cong, P\. Wang, Q\. Wang, Q\. Zhu, Q\. Li, Q\. Chen, Q\. Du, R\. Xu, R\. Ge, R\. Zhang, R\. Pan, R\. Wang, R\. Yin, R\. Xu, R\. Shen, R\. Zhang, S\. H\. Liu, S\. Lu, S\. Zhou, S\. Chen, S\. Cai, S\. Chen, S\. Hu, S\. Liu, S\. Hu, S\. Ma, S\. Wang, S\. Yu, S\. Zhou, S\. Pan, S\. Zhou, T\. Ni, T\. Yun, T\. Pei, T\. Ye, T\. Yue, W\. Zeng, W\. Liu, W\. Liang, W\. Pang, W\. Luo, W\. Gao, W\. Zhang, X\. Gao, X\. Wang, X\. Bi, X\. Liu, X\. Wang, X\. Chen, X\. Zhang, X\. Nie, X\. Cheng, X\. Liu, X\. Xie, X\. Liu, X\. Yu, X\. Li, X\. Yang, X\. Li, X\. Chen, X\. Su, X\. Pan, X\. Lin, X\. Fu, Y\. Q\. Wang, Y\. Zhang, Y\. Xu, Y\. Ma, Y\. Li, Y\. Li, Y\. Zhao, Y\. Sun, Y\. Wang, Y\. Qian, Y\. Yu, Y\. Zhang, Y\. Ding, Y\. Shi, Y\. Xiong, Y\. He, Y\. Zhou, Y\. Zhong, Y\. Piao, Y\. Wang, Y\. Chen, Y\. Tan, Y\. Wei, Y\. Ma, Y\. Liu, Y\. Yang, Y\. Guo, Y\. Wu, Y\. Wu, Y\. Cheng, Y\. Ou, Y\. Xu, Y\. Wang, Y\. Gong, Y\. Wu, Y\. Zou, Y\. Li, Y\. Xiong, Y\. Luo, Y\. You, Y\. Liu, Y\. Zhou, Z\. F\. Wu, Z\. Z\. Ren, Z\. Zhao, Z\. Ren, Z\. Sha, Z\. Fu, Z\. Xu, Z\. Xie, Z\. Zhang, Z\. Hao, Z\. Gou, Z\. Ma, Z\. Yan, Z\. Shao, Z\. Huang, Z\. Wu, Z\. Li, Z\. Zhang, Z\. Xu, Z\. Wang, Z\. Gu, Z\. Zhu, Z\. Li, Z\. Zhang, Z\. Xie, Z\. Gao, Z\. Pan, Z\. Yao, B\. Feng, H\. Li, J\. L\. Cai, J\. Ni, L\. Xu, M\. Li, N\. Tian, R\. J\. Chen, R\. L\. Jin, S\. S\. Li, S\. Zhou, T\. Sun, X\. Q\. Li, X\. Jin, X\. Shen, X\. Chen, X\. Song, X\. Zhou, Y\. X\. Zhu, Y\. Huang, Y\. Li, Y\. Zheng, Y\. Zhu, Y\. Ma, Z\. Huang, Z\. Xu, Z\. Zhang, D\. Ji, J\. Liang, J\. Guo, J\. Chen, L\. Xia, M\. Wang, M\. Li, P\. Zhang, R\. Chen, S\. Sun, S\. Wu, S\. Ye, T\. Wang, W\. L\. Xiao, W\. An, X\. Wang, X\. Sun, X\. Wang, Y\. Tang, Y\. Zha, Z\. Zhang, Z\. Ju, Z\. Zhang, and Z\. Qu \(2025\)DeepSeek\-v3\.2: pushing the frontier of open large language models\.External Links:2512\.02556,[Link](https://arxiv.org/abs/2512.02556)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- B\. Gao, F\. Song, Z\. Yang, Z\. Cai, Y\. Miao, Q\. Dong, L\. Li, C\. Ma, L\. Chen, R\. Xu, Z\. Tang, B\. Wang, D\. Zan, S\. Quan, G\. Zhang, L\. Sha, Y\. Zhang, X\. Ren, T\. Liu, and B\. Chang \(2024\)Omni\-math: a universal olympiad level mathematic benchmark for large language models\.External Links:2410\.07985,[Link](https://arxiv.org/abs/2410.07985)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- Google DeepMind \(2026\)Gemini 3\.1 Pro: Model Card\.Note:[https://deepmind\.google/models/model\-cards/gemini\-3\-1\-pro/](https://deepmind.google/models/model-cards/gemini-3-1-pro/)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- D\. Guo, D\. Yang, H\. Zhang, J\. Song, P\. Wang, Q\. Zhu, R\. Xu, R\. Zhang, S\. Ma, X\. Bi,et al\.\(2025\)DeepSeek\-r1 incentivizes reasoning in llms through reinforcement learning\.Nature645\(8081\),pp\. 633–638\.Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1)\.
- C\. He, R\. Luo, Y\. Bai, S\. Hu, Z\. Thai, J\. Shen, J\. Hu, X\. Han, Y\. Huang, Y\. Zhang, J\. Liu, L\. Qi, Z\. Liu, and M\. Sun \(2024\)OlympiadBench: a challenging benchmark for promoting AGI with olympiad\-level bilingual multimodal scientific problems\.InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),L\. Ku, A\. Martins, and V\. Srikumar \(Eds\.\),Bangkok, Thailand,pp\. 3828–3850\.External Links:[Link](https://aclanthology.org/2024.acl-long.211/),[Document](https://dx.doi.org/10.18653/v1/2024.acl-long.211)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. Steinhardt \(2021\)Measuring mathematical problem solving with the MATH dataset\.InThirty\-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track \(Round 2\),External Links:[Link](https://openreview.net/forum?id=7Bywt2mQsCe)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom,et al\.\(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature,pp\. 1–3\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- A\. Jaech, A\. Kalai, A\. Lerer, A\. Richardson, A\. El\-Kishky, A\. Low, A\. Helyar, A\. Madry, A\. Beutel, A\. Carney,et al\.\(2024\)Openai o1 system card\.arXiv preprint arXiv:2412\.16720\.Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1)\.
- J\. Jiang, W\. He, W\. Yuefeng, G\. Gao, Y\. Hu, J\. Wang, N\. Guan, P\. Wu, B\. Dai, L\. Xiao, and B\. Dong \(2026\)FATE: a formal benchmark series for frontier algebra of multiple difficulty levels\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=3bD19r4jqh)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- Y\. Li, D\. Du, L\. Song, C\. Li, W\. Wang, T\. Yang, and H\. Mi \(2024\)Hunyuanprover: a scalable data synthesis framework and guided tree search for automated theorem proving\.arXiv preprint arXiv:2412\.20735\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. Jin \(2025\)Goedel\-prover\-v2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.External Links:2508\.03613,[Link](https://arxiv.org/abs/2508.03613)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1),[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1),[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- C\. Liu, J\. Shen, H\. Xin, Z\. Liu, Y\. Yuan, H\. Wang, W\. Ju, C\. Zheng, Y\. Yin, L\. Li, M\. Zhang, and Q\. Liu \(2023\)FIMO: a challenge formal dataset for automated theorem proving\.External Links:2309\.04295,[Link](https://arxiv.org/abs/2309.04295)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- J\. Liu, X\. Lin, J\. Bayer, Y\. Dillies, W\. Jiang, X\. Liang, R\. Soletskyi, H\. Wang, Y\. Xie, B\. Xiong,et al\.\(2025\)Combibench: benchmarking llm capability for combinatorial mathematics\.arXiv preprint arXiv:2505\.03171\.Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- J\. Liu, Z\. Zhou, Z\. Zhu, M\. D\. Santos, W\. He, J\. Liu, R\. Wang, Y\. Xie, J\. Zhao, Q\. Wang,et al\.\(2026\)Numina\-lean\-agent: an open and general agentic reasoning system for formal mathematics\.arXiv preprint arXiv:2601\.14027\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- T\. Luong, D\. Hwang, H\. H\. Nguyen, G\. Ghiasi, Y\. Chervonyi, I\. Seo, J\. Kim, G\. Bingham, J\. Lee, S\. Mishra, A\. Zhai, H\. Hu, H\. Michalewski, J\. Kim, J\. Ahn, J\. Bae, X\. Song, T\. H\. Trinh, Q\. V\. Le, and J\. Jung \(2025\)Towards robust mathematical reasoning\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,C\. Christodoulopoulos, T\. Chakraborty, C\. Rose, and V\. Peng \(Eds\.\),Suzhou, China,pp\. 35418–35442\.External Links:[Link](https://aclanthology.org/2025.emnlp-main.1794/),[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.1794),ISBN 979\-8\-89176\-332\-6Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- W\. Ma, A\. Cojocaru, N\. Kolhe, R\. Sharif, H\. Zhang, V\. Zhuang, M\. Zaharia, and S\. Min \(2025\)Reliable fine\-grained evaluation of natural language math proofs\.InThe 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025,External Links:[Link](https://openreview.net/forum?id=9wGudIBTXg)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- \[27\]MAAAmerican invitational mathematics examination\-aime\.External Links:[Link](https://maa.org/maa-invitational-competitions/)Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- T\. mathlib Community \(2020\)The lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,CPP 2020,New York, NY, USA,pp\. 367–381\.External Links:ISBN 9781450370974,[Link](https://doi.org/10.1145/3372885.3373824),[Document](https://dx.doi.org/10.1145/3372885.3373824)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p2.3)\.
- L\. d\. Moura and S\. Ullrich \(2021\)The lean 4 theorem prover and programming language\.InInternational Conference on Automated Deduction,pp\. 625–635\.Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1)\.
- NVIDIA \(2025\)Nemotron 3 Nano: open, efficient mixture\-of\-experts hybrid Mamba\-Transformer model for Agentic reasoning\.Note:Technical reportExternal Links:[Link](https://arxiv.org/abs/2512.20848)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- OpenAI \(2025\)Gpt\-oss\-120b & gpt\-oss\-20b model card\.External Links:2508\.10925,[Link](https://arxiv.org/abs/2508.10925)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- OpenAI \(2026\)Introducing GPT\-5\.5\.Note:[https://openai\.com/index/introducing\-gpt\-5\-5/](https://openai.com/index/introducing-gpt-5-5/)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- A\. Ospanov, F\. Farnia, and R\. Yousefzadeh \(2026\)MiniF2F\-lean revisited: reviewing limitations and charting a path forward\.InThe Thirty\-ninth Annual Conference on Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=KtaHv0YUyh)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- Qwen Team \(2026\)Qwen3\.5: towards native multimodal agents\.External Links:[Link](https://qwen.ai/blog?id=qwen3.5)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. Ruan \(2025\)DeepSeek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.External Links:2504\.21801,[Link](https://arxiv.org/abs/2504.21801)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p1.1),[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1),[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- M\. D\. Santos, H\. de Saxcé, H\. Wang, R\. Wang, M\. Baksys, M\. Unsal, J\. Liu, Z\. Liu, and J\. Li \(2025\)Kimina lean server: a high\-performance lean server for large\-scale verification\.External Links:2504\.21230,[Link](https://arxiv.org/abs/2504.21230)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p2.3)\.
- Z\. Shao, Y\. Luo, C\. Lu, Z\. Z\. Ren, J\. Hu, T\. Ye, Z\. Gou, S\. Ma, and X\. Zhang \(2025\)DeepSeekMath\-v2: towards self\-verifiable mathematical reasoning\.External Links:2511\.22570,[Link](https://arxiv.org/abs/2511.22570)Cited by:[§5\.2](https://arxiv.org/html/2606.13782#S5.SS2.p2.1)\.
- Q\. Team \(2025\)Qwen3 technical report\.External Links:2505\.09388,[Link](https://arxiv.org/abs/2505.09388)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.InAdvances in Neural Information Processing Systems,A\. Globerson, L\. Mackey, D\. Belgrave, A\. Fan, U\. Paquet, J\. Tomczak, and C\. Zhang \(Eds\.\),Vol\.37,pp\. 11545–11569\.External Links:[Document](https://dx.doi.org/10.52202/079017-0368),[Link](https://proceedings.neurips.cc/paper_files/paper/2024/file/1582eaf9e0cf349e1e5a6ee453100aa1-Paper-Datasets_and_Benchmarks_Track.pdf)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. D\. Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu,et al\.\(2025\)Kimina\-prover preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1),[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- Z\. Wu, S\. Huang, Z\. Zhou, H\. Ying, Z\. Yuan, W\. Zhang, D\. Lin, and K\. Chen \(2025\)InternLM2\. 5\-stepprover: advancing automated theorem proving via critic\-guided search\.In2nd AI for Math Workshop@ ICML 2025,Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- H\. Xin, Z\. Z\. Ren, J\. Song, Z\. Shao, W\. Zhao, H\. Wang, B\. Liu, L\. Zhang, X\. Lu, Q\. Du, W\. Gao, Q\. Zhu, D\. Yang, Z\. Gou, Z\. F\. Wu, F\. Luo, and C\. Ruan \(2024\)DeepSeek\-prover\-v1\.5: harnessing proof assistant feedback for reinforcement learning and monte\-carlo tree search\.External Links:2408\.08152,[Link](https://arxiv.org/abs/2408.08152)Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- R\. Xin, C\. Xi, J\. Yang, F\. Chen, H\. Wu, X\. Xiao, Y\. Sun, S\. Zheng, and M\. Ding \(2025\)BFS\-prover: scalable best\-first tree search for llm\-based automatic theorem proving\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 32588–32599\.Cited by:[§2\.1](https://arxiv.org/html/2606.13782#S2.SS1.p1.1)\.
- R\. Xu, H\. Dai, Y\. Fu, J\. Jiang, T\. Nie, H\. Wang, J\. Wang, H\. Yang, J\. Yang, and Z\. Zhang \(2025\)LeanCat: a benchmark suite for formal category theory in lean \(part i: 1\-categories\)\.arXiv preprint arXiv:2512\.24796\.Cited by:[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Z\. Yuan, H\. Xin, W\. Huang, Y\. Wen, G\. Zhang, and W\. Liu \(2025\)FormalMATH: benchmarking formal mathematical reasoning of large language models\.External Links:2505\.02735,[Link](https://arxiv.org/abs/2505.02735)Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.
- Z\.ai \(2026\)GLM\-5: from vibe coding to agentic engineering\.Note:[https://github\.com/zai\-org/GLM\-5](https://github.com/zai-org/GLM-5)Cited by:[§4\.1](https://arxiv.org/html/2606.13782#S4.SS1.p1.1)\.
- K\. Zheng, J\. M\. Han, and S\. Polu \(2022\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.13782#S1.p2.1),[§2\.2](https://arxiv.org/html/2606.13782#S2.SS2.p1.1)\.

## Appendix ACategory Distribution

MA\-ProofBench covers a wide range of analytical topics\. To illustrate its mathematical diversity, Table[4](https://arxiv.org/html/2606.13782#A1.T4)details the distribution of the benchmark’s problems across various Mathematics Subject Classification \(MSC\) categories for both difficulty levels\.

Table 4:Distribution of MA\-ProofBench problems across MSC categories\.Category / Subcategory NameLevel ILevel IIReal FunctionsFunctions of One Variable302Functions of Several Variables62Polynomials, Rational Functions in Real Analysis10Inequalities in Real Analysis68Miscellaneous Topics in Real Functions10Measure and IntegrationClassical Measure Theory1315Set Functions, Measures and Integrals with Values in Abstract Spaces01Set Functions and Measures on Spaces with Additional Structure01Functions of a Complex VariableGeneral Properties of Functions of One Complex Variable92Series Expansions of Functions of One Complex Variable10Geometric Function Theory510Entire and Meromorphic Functions of One Complex Variable, and Related Topics43Miscellaneous Topics of Analysis in the Complex Plane01Sequences, Series, and SummabilityConvergence and Divergence of Infinite Limiting Processes51Functional AnalysisTopological Linear Spaces and Related Structures12Normed Linear Spaces and Banach Spaces; Banach Lattices26Inner Product Spaces and Their Generalizations, Hilbert Spaces20Linear Function Spaces and Their Duals714Distributions, Generalized Functions, Distribution Spaces07Measures, Integration, Derivative, Holomorphy21Commutative Banach Algebras and Commutative Topological Algebras01Nonlinear Functional Analysis10Operator TheoryGeneral Theory of Linear Operators312Special Classes of Linear Operators05Ordinary Differential Operators02Integral, Integro\-Differential, and Pseudodifferential Operators04Nonlinear Operators and Their Properties10Total100100
## Appendix BCase Studies

### B\.1Successful Proofs

Success Case \(DeepSeek\-V3\.2\-Thinking\)Question:Letf∈C2​π​\(ℝ,ℝ\)f\\in C\_\{2\\pi\}\(\\mathbb\{R\},\\mathbb\{R\}\)be differentiable\. Show thatf′f^\{\\prime\}has a zero in\(0,2​π\)\(0,2\\pi\)\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMV84MyB7ZiA6IOKEnSDihpIg4oSdfSAoaHBlciA6IEZ1bmN0aW9uLlBlcmlvZGljIGYgKDIgKiBSZWFsLnBpKSkgKGhkaWZmIDogRGlmZmVyZW50aWFibGUg4oSdIGYpIDoKICAgIOKIgyBjIOKIiCBTZXQuSW9vIDAgKDIgKiBSZWFsLnBpKSwgZGVyaXYgZiBjID0gMCA6PSBieQogIGhhdmUgz4Bwb3MgOiAwIDwgUmVhbC5waSA6PSBSZWFsLnBpX3BvcwogIGhhdmUgaGx0IDogKDAgOiDihJ0pIDwgMiAqIFJlYWwucGkgOj0gYnkgbGluYXJpdGgKICBoYXZlIGhjb250IDogQ29udGludW91c09uIGYgKFNldC5JY2MgMCAoMiAqIFJlYWwucGkpKSA6PQogICAgaGRpZmYuY29udGludW91cy5jb250aW51b3VzT24KICBoYXZlIGhkaWZmX29uIDogRGlmZmVyZW50aWFibGVPbiDihJ0gZiAoU2V0LklvbyAwICgyICogUmVhbC5waSkpIDo9CiAgICBoZGlmZi5kaWZmZXJlbnRpYWJsZU9uCiAgaGF2ZSBoX2VxIDogZiAoMiAqIFJlYWwucGkpID0gZiAwIDo9IGJ5IHNpbXBhIHVzaW5nIGhwZXIgMAogIHJjYXNlcyBleGlzdHNfZGVyaXZfZXFfc2xvcGUgZiBobHQgaGNvbnQgaGRpZmZfb24gd2l0aCDin6hjLCBoYywgaGMn4p+pCiAgcncgW2hfZXEsIHN1Yl9zZWxmLCB6ZXJvX2Rpdl0gYXQgaGMnCiAgZXhhY3Qg4p+oYywgaGMsIGhjJ+KfqQ==)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_83𝒩\\mathcal\{N\}\{f𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\}𝒩\\mathcal\{N\}\(hper𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Function\.Periodic𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi\)\)𝒩\\mathcal\{N\}\(hdiff𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Differentiable𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}c𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}Set\.Ioo𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}\(2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi\),𝒩\\mathcal\{N\}deriv𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}c𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}π\\pipos𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}Real\.pi𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}Real\.pi\_pos𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hlt𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}linarith𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hcont𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ContinuousOn𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(Set\.Icc𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}\(2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi\)\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}hdiff\.continuous\.continuousOn𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hdiff\_on𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}DifferentiableOn𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(Set\.Ioo𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}\(2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi\)\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}hdiff\.differentiableOn𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_eq𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(2𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}Real\.pi\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}simpa𝒩\\mathcal\{N\}using𝒩\\mathcal\{N\}hper𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rcases𝒩\\mathcal\{N\}exists\_deriv\_eq\_slope𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}hlt𝒩\\mathcal\{N\}hcont𝒩\\mathcal\{N\}hdiff\_on𝒩\\mathcal\{N\}with𝒩\\mathcal\{N\}⟨\\langlec,𝒩\\mathcal\{N\}hc,𝒩\\mathcal\{N\}hc’⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[h\_eq,𝒩\\mathcal\{N\}sub\_self,𝒩\\mathcal\{N\}zero\_div\]𝒩\\mathcal\{N\}at𝒩\\mathcal\{N\}hc’𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}⟨\\langlec,𝒩\\mathcal\{N\}hc,𝒩\\mathcal\{N\}hc’⟩\\rangleAnalysis:The model successfully proves the existence of a zero for the derivative of a differentiable periodic function\. It accurately identifies and applies the Mean Value Theorem \(exists\_deriv\_eq\_slope\) from Mathlib\. By verifying the prerequisites of continuity and differentiability on the appropriate intervals, it cleverly uses the periodicity condition to deduce a zero slope, effectively concluding the proof\.

Success Case \(Gemini 3\.1 Pro\)Question:LetHHbe a Hilbert space and letUUbe a bounded linear operator acting onHH\. IfUUis a unitary operator, andσ​\(U\)\\sigma\(U\)denotes the spectrum ofUU, prove thatσ​\(U\)⊆\{z∈ℂ:\|z\|=1\}\\sigma\(U\)\\subseteq\\\{z\\in\\mathbb\{C\}:\|z\|=1\\\}\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMl83MyAoSCA6IFR5cGUqKSBbTm9ybWVkQWRkQ29tbUdyb3VwIEhdIFtJbm5lclByb2R1Y3RTcGFjZSDihIIgSF0gW0NvbXBsZXRlU3BhY2UgSF0KICAgIChVIDogSCDihpJMW+KEgl0gSCkKICAgICho4oKBIDogVS5hZGpvaW50ICogVSA9IDEpICho4oKCIDogVSAqIFUuYWRqb2ludCA9IDEpIDoKICAgIHNwZWN0cnVtIOKEgiBVIOKKhiB7eiA6IOKEgiB8IOKAlnrigJYgPSAxfSA6PSBieQogIC0tIEluIHRoZSBDKi1hbGdlYnJhIG9mIGNvbnRpbnVvdXMgbGluZWFyIG1hcHMgYEgg4oaSTFvihIJdIEhgLCBgc3RhciBVYCBpcyBkZWZpbml0aW9uYWxseSBgVS5hZGpvaW50YAogIGhhdmUgaDFfc3RhciA6IHN0YXIgVSAqIFUgPSAxIDo9IGjigoEKICBoYXZlIGgyX3N0YXIgOiBVICogc3RhciBVID0gMSA6PSBo4oKCCgogIC0tIFdlIGNvbnN0cnVjdCB0aGUgcHJvb2YgdGhhdCBVIGJlbG9uZ3MgdG8gdGhlIHVuaXRhcnkgc3VibW9ub2lkCiAgaGF2ZSBodSA6IFUg4oiIIHVuaXRhcnkgKEgg4oaSTFvihIJdIEgpIDo9IOKfqGgxX3N0YXIsIGgyX3N0YXLin6kKICBsZXQgdSA6IHVuaXRhcnkgKEgg4oaSTFvihIJdIEgpIDo9IOKfqFUsIGh14p+pCgogIC0tIEFwcGx5IHRoZSBnZW5lcmFsIEMqLWFsZ2VicmEgdGhlb3JlbSB0aGF0IGJvdW5kcyB0aGUgc3BlY3RydW0gb2YgYSB1bml0YXJ5IGVsZW1lbnQKICAtLSB0byBiZSB3aXRoaW4gdGhlIG1ldHJpYyBzcGhlcmUgb2YgcmFkaXVzIDEgY2VudGVyZWQgYXQgMC4KICBoYXZlIGhfc3BlYyA6IHNwZWN0cnVtIOKEgiAodSA6IEgg4oaSTFvihIJdIEgpIOKKhiBNZXRyaWMuc3BoZXJlICgwIDog4oSCKSAxIDo9CiAgICB1bml0YXJ5LnNwZWN0cnVtX3N1YnNldF9jaXJjbGUgdQoKICAtLSBOb3cgd2Ugc2ltcGx5IHRyYW5zbGF0ZSB0aGUgYE1ldHJpYy5zcGhlcmVgIGNvbmRpdGlvbiB0byB0aGUgZ29hbCdzIG5vcm0gY29uZGl0aW9uCiAgaW50cm8geiBoegogIGhhdmUgaHonIDo9IGhfc3BlYyBoegoKICAtLSBgeiDiiIggTWV0cmljLnNwaGVyZSAwIDFgIG1lYW5zIGBkaXN0IHogMCA9IDFgLgogIC0tIFNpbmNlIGBkaXN0IHogMCA9IOKAlnrigJZgLCBpdCBzaW1wbGlmaWVzIGV4YWN0bHkgdG8gYOKAlnrigJYgPSAxYC4KICBydyBbTWV0cmljLm1lbV9zcGhlcmUsIGRpc3RfemVyb19yaWdodF0gYXQgaHonCiAgZXhhY3QgaHon)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l2\_73𝒩\\mathcal\{N\}\(H𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Type\*\)𝒩\\mathcal\{N\}\[NormedAddCommGroup𝒩\\mathcal\{N\}H\]𝒩\\mathcal\{N\}\[InnerProductSpace𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}H\]𝒩\\mathcal\{N\}\[CompleteSpace𝒩\\mathcal\{N\}H\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(U𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}H𝒩\\mathcal\{N\}→\\toL\[ℂ\\mathbb\{C\}\]𝒩\\mathcal\{N\}H\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(h1𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}U\.adjoint𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}1\)𝒩\\mathcal\{N\}\(h2𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}U\.adjoint𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}1\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}spectrum𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}⊆\\subseteq𝒩\\mathcal\{N\}\{z𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}\|𝒩\\mathcal\{N\}∥\\\|z∥\\\|𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}1\}𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h1\_star𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}star𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h1𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h2\_star𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}star𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h2𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hu𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}U𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}unitary𝒩\\mathcal\{N\}\(H𝒩\\mathcal\{N\}→\\toL\[ℂ\\mathbb\{C\}\]𝒩\\mathcal\{N\}H\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}⟨\\langleh1\_star,𝒩\\mathcal\{N\}h2\_star⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}let𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}unitary𝒩\\mathcal\{N\}\(H𝒩\\mathcal\{N\}→\\toL\[ℂ\\mathbb\{C\}\]𝒩\\mathcal\{N\}H\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}⟨\\langleU,𝒩\\mathcal\{N\}hu⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_spec𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}spectrum𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}𝒩\\mathcal\{N\}\(u𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}H𝒩\\mathcal\{N\}→\\toL\[ℂ\\mathbb\{C\}\]𝒩\\mathcal\{N\}H\)𝒩\\mathcal\{N\}⊆\\subseteq𝒩\\mathcal\{N\}Metric\.sphere𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℂ\\mathbb\{C\}\)𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}unitary\.spectrum\_subset\_circle𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}intro𝒩\\mathcal\{N\}z𝒩\\mathcal\{N\}hz𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hz’𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h\_spec𝒩\\mathcal\{N\}hz𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[Metric\.mem\_sphere,𝒩\\mathcal\{N\}dist\_zero\_right\]𝒩\\mathcal\{N\}at𝒩\\mathcal\{N\}hz’𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}hz’Analysis:This example demonstrates the model’s proficiency in handling advanced functional analysis concepts\. To bound the spectrum of a unitary operator on a Hilbert space, the model avoids reasoning from first principles and instead expertly navigates Mathlib’s C\*\-algebra API\. It explicitly constructs the unitary submonoid to apply the general theoremunitary\.spectrum\_subset\_circle, and then smoothly translates the topological metric condition \(Metric\.sphere\) into the algebraic norm condition required by the goal\.

### B\.2Failed Proofs

Failure Case: Mathlib Hallucination \(DeepSeek\-Prover\-V2\-671B\)Question:Verify thatg:ℝ2∖\{0\}→ℝg:\\mathbb\{R\}^\{2\}\\setminus\\\{0\\\}\\to\\mathbb\{R\}defined byg​\(x\):=log⁡\|x\|,g\(x\):=\\log\|x\|,is harmonic inℝ2∖\{0\}\\mathbb\{R\}^\{2\}\\setminus\\\{0\\\}\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMV81MCA6IElubmVyUHJvZHVjdFNwYWNlLkhhcm1vbmljT25OaGQgKGZ1biB4IDogRXVjbGlkZWFuU3BhY2Ug4oSdIChGaW4gMikgPT4gUmVhbC5sb2cg4oCWeOKAlikgKHswfeG2nCkgOj0gYnkKICBoYXZlIGhfbWFpbiA6IOKIgCAoeCA6IEV1Y2xpZGVhblNwYWNlIOKEnSAoRmluIDIpKSwgeCDiiIggKHswfeG2nCA6IFNldCAoRXVjbGlkZWFuU3BhY2Ug4oSdIChGaW4gMikpKSDihpIg4oiDICh1IDogU2V0IChFdWNsaWRlYW5TcGFjZSDihJ0gKEZpbiAyKSkpIChodSA6IHUg4oiIICgqQCRcbWF0aGNhbHtOfSRAKilbKHswfeG2nCA6IFNldCAoRXVjbGlkZWFuU3BhY2Ug4oSdIChGaW4gMikpKV0geCksICgqQFxjb2xvcmJveHtwaW5rfXtcdGV4dGJme0lubmVyUHJvZHVjdFNwYWNlLkhhcm1vbmljT259fUAqKSAoZnVuIHggOiBFdWNsaWRlYW5TcGFjZSDihJ0gKEZpbiAyKSA9PiBSZWFsLmxvZyDigJZ44oCWKSB1IDo9IGJ5CiAgICBpbnRybyB4IGh4CiAgICBoYXZlIGh4JyA6IHgg4omgIDAgOj0gYnkgc2ltcGEgdXNpbmcgaHgKICAgIHVzZSAoezB94bacIDogU2V0IChFdWNsaWRlYW5TcGFjZSDihJ0gKEZpbiAyKSkpCiAgICB1c2U/CiAgICAoKkBcY29sb3Jib3h7cGlua317XHRleHRiZntzb3JyeX19QCopCiAgaW50cm8geCBoeAogIGhhdmUgaOKCgSA6IOKIgyAodSA6IFNldCAoRXVjbGlkZWFuU3BhY2Ug4oSdIChGaW4gMikpKSAoaHUgOiB1IOKIiCAoKkAkXG1hdGhjYWx7Tn0kQCopWyh7MH3htpwgOiBTZXQgKEV1Y2xpZGVhblNwYWNlIOKEnSAoRmluIDIpKSldIHgpLCAoKkBcY29sb3Jib3h7cGlua317XHRleHRiZntJbm5lclByb2R1Y3RTcGFjZS5IYXJtb25pY09ufX1AKikgKGZ1biB4IDogRXVjbGlkZWFuU3BhY2Ug4oSdIChGaW4gMikgPT4gUmVhbC5sb2cg4oCWeOKAlikgdSA6PSBieQogICAgYXBwbHkgaF9tYWluCiAgICBleGFjdCBoeAogIG9idGFpbiDin6h1LCBodSwgaOKCguKfqSA6PSBo4oKBCiAgZXhhY3Qg4p+odSwgaHUsIGjigoLin6k=)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_50𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}InnerProductSpace\.HarmonicOnNhd𝒩\\mathcal\{N\}\(fun𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)𝒩\\mathcal\{N\}=\>𝒩\\mathcal\{N\}Real\.log𝒩\\mathcal\{N\}∥\\\|x∥\\\|\)𝒩\\mathcal\{N\}\(\{0\}c\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_main𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}\(x𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\),𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}\(\{0\}c𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}\(u𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)𝒩\\mathcal\{N\}\(hu𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\[\(\{0\}c𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)\]𝒩\\mathcal\{N\}x\),𝒩\\mathcal\{N\}InnerProductSpace\.HarmonicOn𝒩\\mathcal\{N\}\(fun𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)𝒩\\mathcal\{N\}=\>𝒩\\mathcal\{N\}Real\.log𝒩\\mathcal\{N\}∥\\\|x∥\\\|\)𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}intro𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hx’𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}≠\\neq𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}simpa𝒩\\mathcal\{N\}using𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}use𝒩\\mathcal\{N\}\(\{0\}c𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}use?𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}sorry𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}intro𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h1𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}\(u𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)𝒩\\mathcal\{N\}\(hu𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\[\(\{0\}c𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}\(EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)\)\)\]𝒩\\mathcal\{N\}x\),𝒩\\mathcal\{N\}InnerProductSpace\.HarmonicOn𝒩\\mathcal\{N\}\(fun𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}EuclideanSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}\(Fin𝒩\\mathcal\{N\}2\)𝒩\\mathcal\{N\}=\>𝒩\\mathcal\{N\}Real\.log𝒩\\mathcal\{N\}∥\\\|x∥\\\|\)𝒩\\mathcal\{N\}u𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}apply𝒩\\mathcal\{N\}h\_main𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}obtain𝒩\\mathcal\{N\}⟨\\langleu,𝒩\\mathcal\{N\}hu,𝒩\\mathcal\{N\}h2⟩\\rangle𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h1𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}⟨\\langleu,𝒩\\mathcal\{N\}hu,𝒩\\mathcal\{N\}h2⟩\\rangleAnalysis:This proof fails due to aMathlib Hallucination\. The model fabricates a nonexistent theorem identifier,InnerProductSpace\.HarmonicOn\. In Mathlib 4, the correct identifier for this context should beInnerProductSpace\.HarmonicOnNhd\. Additionally, the model is unable to resolve the neighborhood filter logic and ultimately resorts to an explicitsorryto bypass the sub\-goal\.

Failure Case: Type System Error \(DeepSeek\-Prover\-V2\-7B\)Question:Supposeν,ν1,ν2\\nu,\\nu\_\{1\},\\nu\_\{2\}are signed measures on\(X,ℳ\)\(X,\\mathcal\{M\}\)andμ\\mua \(positive\) measure onℳ\\mathcal\{M\}\. Proveν1⟂ν2\\nu\_\{1\}\\perp\\nu\_\{2\}implies\|ν1\|⟂\|ν2\|\|\\nu\_\{1\}\|\\perp\|\\nu\_\{2\}\|\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMV85OCB7WCA6IFR5cGUqfSBbTWVhc3VyYWJsZVNwYWNlIFhdCiAgICAozr3igoEgzr3igoIgOiBNZWFzdXJlVGhlb3J5LlNpZ25lZE1lYXN1cmUgWCkKICAgIChoIDogTWVhc3VyZVRoZW9yeS5WZWN0b3JNZWFzdXJlLk11dHVhbGx5U2luZ3VsYXIgzr3igoEgzr3igoIpIDoKICAgIChNZWFzdXJlVGhlb3J5Lk1lYXN1cmUuTXV0dWFsbHlTaW5ndWxhciDOveKCgS50b3RhbFZhcmlhdGlvbiDOveKCgi50b3RhbFZhcmlhdGlvbikgOj0gYnkKICBoYXZlIGhfbWFpbiA6IE1lYXN1cmVUaGVvcnkuTWVhc3VyZS5NdXR1YWxseVNpbmd1bGFyIM694oKBLnRvdGFsVmFyaWF0aW9uIM694oKCLnRvdGFsVmFyaWF0aW9uIDo9IGJ5CiAgICAtLSBVc2UgdGhlIGZhY3QgdGhhdCDOveKCgSBhbmQgzr3igoIgYXJlIG11dHVhbGx5IHNpbmd1bGFyIHRvIGZpbmQgYSBzZXQgQiBzdWNoIHRoYXQgzr3igoEoQikgPSAwIGFuZCDOveKCgihC4bacKSA9IDAKICAgIGhhdmUgaOKCgSA6IOKIgyAoQiA6IFNldCBYKSwgTWVhc3VyYWJsZVNldCBCIOKIpyDOveKCgSBCID0gMCDiiKcgzr3igoIgQuG2nCA9IDAgOj0gYnkKICAgICAgZXhhY3QgaAogICAgb2J0YWluIOKfqEIsIGhCX20sIGhC4oKBLCBoQuKCguKfqSA6PSBo4oKBCiAgICAtLSBTaG93IHRoYXQgdGhlIHRvdGFsIHZhcmlhdGlvbiBvZiDOveKCgSBhdCBCIGlzIDAKICAgIGhhdmUgaOKCgiA6IM694oKBLnRvdGFsVmFyaWF0aW9uIEIgPSAwIDo9IGJ5CiAgICAgIC0tIENvbXB1dGUgdGhlIHRvdGFsIHZhcmlhdGlvbiBvZiDOveKCgSBhdCBCCiAgICAgIGhhdmUgaOKCgyA6ICgqQFxjb2xvcmJveHtwaW5rfXtcdGV4dGJmeyRcbnVfMSQudG90YWxWYXJpYXRpb24gQiA9IHwkXG51XzEkIEJ8fX1AKikgOj0gYnkKICAgICAgICAtLSBVc2UgdGhlIGRlZmluaXRpb24gb2YgdG90YWwgdmFyaWF0aW9uIGZvciBhIHNpZ25lZCBtZWFzdXJlCiAgICAgICAgc2ltcCBbTWVhc3VyZVRoZW9yeS5TaWduZWRNZWFzdXJlLnRvdGFsVmFyaWF0aW9uLCBhYnNfZXFfc2VsZi5tcHIgKGxlX29mX2x0IChzaG93ICgwIDog4oSd4omlMCkgPCAxIGJ5IG5vcm1fbnVtKSldCiAgICAgIHJ3IFto4oKDXQogICAgICAtLSBTaW1wbGlmeSB8zr3igoEgQnwgc2luY2Ugzr3igoEgQiA9IDAKICAgICAgaGF2ZSBo4oKEIDogfM694oKBIEJ8ID0gMCA6PSBieQogICAgICAgIHNpbXAgW2hC4oKBXQogICAgICAgIDw7PiBhZXNvcAogICAgICBydyBbaOKChF0KICAgIC0tIFNob3cgdGhhdCB0aGUgdG90YWwgdmFyaWF0aW9uIG9mIM694oKCIGF0IELhtpwgaXMgMAogICAgaGF2ZSBo4oKDIDogzr3igoIudG90YWxWYXJpYXRpb24gQuG2nCA9IDAgOj0gYnkKICAgICAgLS0gQ29tcHV0ZSB0aGUgdG90YWwgdmFyaWF0aW9uIG9mIM694oKCIGF0IELhtpwKICAgICAgaGF2ZSBo4oKEIDogKCpAXGNvbG9yYm94e3Bpbmt9e1x0ZXh0YmZ7JFxudV8yJC50b3RhbFZhcmlhdGlvbiBCJF57XG1hdGhybXtjfX0kID0gfCRcbnVfMiQgQiRee1xtYXRocm17Y319JHx9fUAqKSA6PSBieQogICAgICAgIC0tIFVzZSB0aGUgZGVmaW5pdGlvbiBvZiB0b3RhbCB2YXJpYXRpb24gZm9yIGEgc2lnbmVkIG1lYXN1cmUKICAgICAgICBzaW1wIFtNZWFzdXJlVGhlb3J5LlNpZ25lZE1lYXN1cmUudG90YWxWYXJpYXRpb24sIGFic19lcV9zZWxmLm1wciAobGVfb2ZfbHQgKHNob3cgKDAgOiDihJ3iiaUwKSA8IDEgYnkgbm9ybV9udW0pKV0KICAgICAgcncgW2jigoRdCiAgICAgIC0tIFNpbXBsaWZ5IHzOveKCgiBC4bacfCBzaW5jZSDOveKCgiBC4bacID0gMAogICAgICBoYXZlIGjigoUgOiB8zr3igoIgQuG2nHwgPSAwIDo9IGJ5CiAgICAgICAgc2ltcCBbaELigoJdCiAgICAgICAgPDs+IGFlc29wCiAgICAgIHJ3IFto4oKFXQogICAgLS0gQ29uY2x1ZGUgdGhhdCDOveKCgS50b3RhbFZhcmlhdGlvbiBhbmQgzr3igoIudG90YWxWYXJpYXRpb24gYXJlIG11dHVhbGx5IHNpbmd1bGFyCiAgICByZWZpbmUnIOKfqEIsIGhCX20sIF/in6kKICAgIHNpbXBfYWxsIFtNZWFzdXJlVGhlb3J5Lk1lYXN1cmUuTXV0dWFsbHlTaW5ndWxhciwgaOKCgiwgaOKCg10KICAgIDw7PiBhZXNvcAogIGV4YWN0IGhfbWFpbg==)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_98𝒩\\mathcal\{N\}\{X𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Type\*\}𝒩\\mathcal\{N\}\[MeasurableSpace𝒩\\mathcal\{N\}X\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(ν\\nu1𝒩\\mathcal\{N\}ν\\nu2𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}MeasureTheory\.SignedMeasure𝒩\\mathcal\{N\}X\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(h𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}MeasureTheory\.VectorMeasure\.MutuallySingular𝒩\\mathcal\{N\}ν\\nu1𝒩\\mathcal\{N\}ν\\nu2\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(MeasureTheory\.Measure\.MutuallySingular𝒩\\mathcal\{N\}ν\\nu1\.totalVariation𝒩\\mathcal\{N\}ν\\nu2\.totalVariation\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_main𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}MeasureTheory\.Measure\.MutuallySingular𝒩\\mathcal\{N\}ν\\nu1\.totalVariation𝒩\\mathcal\{N\}ν\\nu2\.totalVariation𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h1𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}\(B𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}X\),𝒩\\mathcal\{N\}MeasurableSet𝒩\\mathcal\{N\}B𝒩\\mathcal\{N\}∧\\wedge𝒩\\mathcal\{N\}ν\\nu1𝒩\\mathcal\{N\}B𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}∧\\wedge𝒩\\mathcal\{N\}ν\\nu2𝒩\\mathcal\{N\}Bc𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}h𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}obtain𝒩\\mathcal\{N\}⟨\\langleB,𝒩\\mathcal\{N\}hB\_m,𝒩\\mathcal\{N\}hB1,𝒩\\mathcal\{N\}hB2⟩\\rangle𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h1𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h2𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ν\\nu1\.totalVariation𝒩\\mathcal\{N\}B𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h3𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ν1\\nu\_\{1\}\.totalVariation B = \|ν1\\nu\_\{1\}B\|𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}\[MeasureTheory\.SignedMeasure\.totalVariation,𝒩\\mathcal\{N\}abs\_eq\_self\.mpr𝒩\\mathcal\{N\}\(le\_of\_lt𝒩\\mathcal\{N\}\(show𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}≥\\geq0\)𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}norm\_num\)\)\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[h3\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h4𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\|ν\\nu1𝒩\\mathcal\{N\}B\|𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}\[hB1\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}<;\>𝒩\\mathcal\{N\}aesop𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[h4\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h3𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ν\\nu2\.totalVariation𝒩\\mathcal\{N\}Bc𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h4𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ν2\\nu\_\{2\}\.totalVariation Bc= \|ν2\\nu\_\{2\}Bc\|𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}\[MeasureTheory\.SignedMeasure\.totalVariation,𝒩\\mathcal\{N\}abs\_eq\_self\.mpr𝒩\\mathcal\{N\}\(le\_of\_lt𝒩\\mathcal\{N\}\(show𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}≥\\geq0\)𝒩\\mathcal\{N\}<𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}norm\_num\)\)\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[h4\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h5𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\|ν\\nu2𝒩\\mathcal\{N\}Bc\|𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}\[hB2\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}<;\>𝒩\\mathcal\{N\}aesop𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[h5\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}refine’𝒩\\mathcal\{N\}⟨\\langleB,𝒩\\mathcal\{N\}hB\_m,𝒩\\mathcal\{N\}\_⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simp\_all𝒩\\mathcal\{N\}\[MeasureTheory\.Measure\.MutuallySingular,𝒩\\mathcal\{N\}h2,𝒩\\mathcal\{N\}h3\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}<;\>𝒩\\mathcal\{N\}aesop𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}h\_mainAnalysis:This represents a classicType System Error\. The model attempts to directly equateν1\\nu\_\{1\}\.totalVariation Bwith\|ν1\\nu\_\{1\}B\|\. However, the former evaluates to a measure value of typeENNReal\(extended non\-negative reals\), whereas the latter evaluates to a standard metric value of typeℝ\\mathbb\{R\}\. Placing these two disparate types on opposite sides of an equality operator triggers a strict type mismatch failure during compiler verification\.

Failure Case: Incomplete Proof \(Claude Sonnet 4\.6\)Question:The functionf∈C1​\(ℝ2,ℝ\)f\\in C^\{1\}\(\\mathbb\{R\}^\{2\},\\mathbb\{R\}\)satisfies∂1f=∂2f\\partial\_\{1\}f=\\partial\_\{2\}fandf​\(0,0\)=0f\(0,0\)=0\. Show that there is ag∈C​\(ℝ2,ℝ\)g\\in C\(\\mathbb\{R\}^\{2\},\\mathbb\{R\}\)such thatf​\(x,y\)=g​\(x,y\)​\(x\+y\)f\(x,y\)=g\(x,y\)\(x\+y\)for\(x,y\)∈ℝ2\(x,y\)\\in\\mathbb\{R\}^\{2\}\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMV8wMiB7ZiA6IOKEnSDDlyDihJ0g4oaSIOKEnX0gKGhmIDogQ29udERpZmYg4oSdIDEgZikKICAgIChocGFyIDog4oiAIHAgOiDihJ0gw5cg4oSdLCAoZmRlcml2IOKEnSBmIHApICgxLCAwKSA9IChmZGVyaXYg4oSdIGYgcCkgKDAsIDEpKQogICAgKGgwIDogZiAoMCwgMCkgPSAwKSA6CiAgICDiiIMgZyA6IOKEnSDDlyDihJ0g4oaSIOKEnSwgQ29udGludW91cyBnIOKIpwogICAgICDiiIAgeCB5IDog4oSdLCBmICh4LCB5KSA9IGcgKHgsIHkpICogKHggKyB5KSA6PSBieQogIGxldCBnIDog4oSdIMOXIOKEnSDihpIg4oSdIDo9IGZ1biBwID0+CiAgICBpZiBwLjEgKyBwLjIgPSAwIHRoZW4KICAgICAgKGZkZXJpdiDihJ0gZiAoMCwgMCkpICgxLCAxKSAvIDIKICAgIGVsc2UKICAgICAgZiBwIC8gKHAuMSArIHAuMikKICB1c2UgZwogIGNvbnN0cnVjdG9yCiAgwrcgLS0gQ29udGludWl0eSBvZiBnCiAgICBoYXZlIGhmX2NvbnQgOiBDb250aW51b3VzIGYgOj0gaGYuY29udGludW91cwogICAgaGF2ZSBoZl9kaWZmIDogRGlmZmVyZW50aWFibGUg4oSdIGYgOj0gaGYuZGlmZmVyZW50aWFibGUgbGVfcmZsCiAgICAoKkBcY29sb3Jib3h7cGlua317XHRleHRiZntzb3JyeX19QCopCiAgwrcgaW50cm8geCB5CiAgICBieV9jYXNlcyBoIDogeCArIHkgPSAwCiAgICDCtyBzaW1wIG9ubHkgW2csIGgsIGl0ZV90cnVlLCBtdWxfemVyb10KICAgICAgKCpAXGNvbG9yYm94e3Bpbmt9e1x0ZXh0YmZ7c29ycnl9fUAqKQogICAgwrcgc2ltcCBvbmx5IFtnLCBoLCBpdGVfZmFsc2VdCiAgICAgIGZpZWxkX3NpbXA=)import𝒩\\mathcal\{N\}Mathlibtheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_02𝒩\\mathcal\{N\}\{f𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}×\\times𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\}𝒩\\mathcal\{N\}\(hf𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ContDiff𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}f\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(hpar𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}p𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}×\\times𝒩\\mathcal\{N\}ℝ\\mathbb\{R\},𝒩\\mathcal\{N\}\(fderiv𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}p\)𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}0\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}\(fderiv𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}p\)𝒩\\mathcal\{N\}\(0,𝒩\\mathcal\{N\}1\)\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(h0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(0,𝒩\\mathcal\{N\}0\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∃\\exists𝒩\\mathcal\{N\}g𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}×\\times𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}ℝ\\mathbb\{R\},𝒩\\mathcal\{N\}Continuous𝒩\\mathcal\{N\}g𝒩\\mathcal\{N\}∧\\wedge𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}∀\\forall𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\},𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(x,𝒩\\mathcal\{N\}y\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}g𝒩\\mathcal\{N\}\(x,𝒩\\mathcal\{N\}y\)𝒩\\mathcal\{N\}\*𝒩\\mathcal\{N\}\(x𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}y\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}let𝒩\\mathcal\{N\}g𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}×\\times𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}fun𝒩\\mathcal\{N\}p𝒩\\mathcal\{N\}=\>𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}if𝒩\\mathcal\{N\}p\.1𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}p\.2𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}then𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\(fderiv𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(0,𝒩\\mathcal\{N\}0\)\)𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}1\)𝒩\\mathcal\{N\}/𝒩\\mathcal\{N\}2𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}else𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}p𝒩\\mathcal\{N\}/𝒩\\mathcal\{N\}\(p\.1𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}p\.2\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}use𝒩\\mathcal\{N\}g𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}constructor𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hf\_cont𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Continuous𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}hf\.continuous𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}hf\_diff𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Differentiable𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}hf\.differentiable𝒩\\mathcal\{N\}le\_rfl𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}sorry𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}intro𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}by\_cases𝒩\\mathcal\{N\}h𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}0𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}only𝒩\\mathcal\{N\}\[g,𝒩\\mathcal\{N\}h,𝒩\\mathcal\{N\}ite\_true,𝒩\\mathcal\{N\}mul\_zero\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}sorry𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}only𝒩\\mathcal\{N\}\[g,𝒩\\mathcal\{N\}h,𝒩\\mathcal\{N\}ite\_false\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}field\_simpAnalysis:This output exemplifies anIncomplete Proofcharacterized by explicitsorryinsertion\. While the model correctly defines the piecewise functiong​\(x,y\)g\(x,y\)to satisfy the conditions, it struggles with the substantial logical leaps required to prove the continuity of this piecewise construction at the singularity boundary \(x\+y=0x\+y=0\)\. Consequently, it abandons the proof by insertingsorryplaceholders\.

Failure Case: Lean Syntax Errors \(DeepSeek\-V3\.2\-Thinking\)Question:LetEEbe an n\.v\.s\. and letC⊂EC\\subset Ebe convex\. Deduce thatC¯=Int⁡C¯\\overline\{C\}=\\overline\{\\operatorname\{Int\}C\}wheneverInt⁡C≠∅\.\\operatorname\{Int\}C\\neq\\varnothing\.Output:[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKb3BlbiBTZXQKCnRoZW9yZW0gbWFfcHJvb2ZiZW5jaF9sMV84OCB7RSA6IFR5cGUqfSBbTm9ybWVkQWRkQ29tbUdyb3VwIEVdIFtOb3JtZWRTcGFjZSDihJ0gRV0KICAgIHtDIDogU2V0IEV9IChoQyA6IENvbnZleCDihJ0gQykgKGhJbnQgOiAoaW50ZXJpb3IgQykuTm9uZW1wdHkpIDoKICAgIGNsb3N1cmUgKGludGVyaW9yIEMpID0gY2xvc3VyZSBDIDo9IGJ5CiAgYXBwbHkgU2V0LlN1YnNldC5hbnRpc3ltbQogIMK3IGV4YWN0IGNsb3N1cmVfbW9ubyAoaW50ZXJpb3Jfc3Vic2V0IEMpCiAgwrcgaW50cm8geCBoeAogICAgcmNhc2VzIGhJbnQgd2l0aCDin6h5LCBoeeKfqQogICAgc2V0IGYgOiDihJ0gw5cgRSDihpIgRSA6PSBmdW4gcCA9PiAoMSAtIHAuMSkgKCpAJFxjZG90JEAqKSB5ICsgcC4xICgqQCRcY2RvdCRAKikgcC4yIHdpdGggaGZfZGVmCiAgICBoYXZlIGhfY29udCA6IENvbnRpbnVvdXMgZiA6PSBieQogICAgICB1bmZvbGQgZgogICAgICBjb250aW51aXR5CiAgICBoYXZlIGhfY29udF9hdCA6IENvbnRpbnVvdXNBdCBmICgxLCB4KSA6PSBoX2NvbnQuY29udGludW91c0F0CiAgICBoYXZlIGhfY2xvc3VyZSA6ICgxLCB4KSDiiIggY2xvc3VyZSAoSW9vICgwIDog4oSdKSAxIMOXy6IgQykgOj0gYnkKICAgICAgcncgW2Nsb3N1cmVfcHJvZF9lcV0KICAgICAgY29uc3RydWN0b3IKICAgICAgwrcgaGF2ZSA6ICgxIDog4oSdKSDiiIggY2xvc3VyZSAoSW9vICgwIDog4oSdKSAxKSA6PSBieQogICAgICAgICAgcncgW2Nsb3N1cmVfSW9vIChieSBub3JtX251bSldCiAgICAgICAgICBleGFjdCDin6hieSBub3JtX251bSwgYnkgbm9ybV9udW3in6kKICAgICAgICBleGFjdCB0aGlzCiAgICAgIMK3IGV4YWN0IGh4CiAgICBoYXZlIGhfaW1hZ2UgOiBmICcnIChJb28gKDAgOiDihJ0pIDEgw5fLoiBDKSDiioYgaW50ZXJpb3IgQyA6PSBieQogICAgICByaW50cm8gXyDin6jin6goKkBcY29sb3Jib3h7cGlua317XHRleHRiZnskXGxhbWJkYSR9fUAqKSwgd+KfqSwg4p+o4p+oaM67MSwgaM67MuKfqSwgaHfin6ksIHJmbOKfqQogICAgICB1bmZvbGQgZgogICAgICBoYXZlIEggOiAoKkBcY29sb3Jib3h7cGlua317XHRleHRiZnskXGxhbWJkYSR9fUAqKSAoKkAkXGNkb3QkQCopIHcgKyAoMSAtICgqQFxjb2xvcmJveHtwaW5rfXtcdGV4dGJmeyRcbGFtYmRhJH19QCopKSAoKkAkXGNkb3QkQCopIHkg4oiIIGludGVyaW9yIEMgOj0KICAgICAgICBoQy5jb21ib19pbnRlcmlvcl9zZWxmX3N1YnNldF9pbnRlcmlvciBodyBoeSAoYnkgbGluYXJpdGgpIChieSBsaW5hcml0aCkgKGJ5IHJpbmcpCiAgICAgIHNpbXBhIFthZGRfY29tbV0gdXNpbmcgSAogICAgaGF2ZSBIMSA6IGYgKDEsIHgpIOKIiCBjbG9zdXJlIChmICcnIChJb28gKDAgOiDihJ0pIDEgw5fLoiBDKSkgOj0KICAgICAgaF9jb250X2F0Lm1lbV9jbG9zdXJlX2ltYWdlIGhfY2xvc3VyZQogICAgaGF2ZSBIMiA6IGNsb3N1cmUgKGYgJycgKElvbyAoMCA6IOKEnSkgMSDDl8uiIEMpKSDiioYgY2xvc3VyZSAoaW50ZXJpb3IgQykgOj0KICAgICAgY2xvc3VyZV9tb25vIGhfaW1hZ2UKICAgIGhhdmUgOiBmICgxLCB4KSA9IHggOj0gYnkgc2ltcCBbZl0KICAgIHJ3IFt0aGlzXSBhdCBIMQogICAgZXhhY3QgSDIgSDE=)import𝒩\\mathcal\{N\}Mathlibopen𝒩\\mathcal\{N\}Settheorem𝒩\\mathcal\{N\}ma\_proofbench\_l1\_88𝒩\\mathcal\{N\}\{E𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Type\*\}𝒩\\mathcal\{N\}\[NormedAddCommGroup𝒩\\mathcal\{N\}E\]𝒩\\mathcal\{N\}\[NormedSpace𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}E\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}\{C𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Set𝒩\\mathcal\{N\}E\}𝒩\\mathcal\{N\}\(hC𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Convex𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}\(hInt𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\(interior𝒩\\mathcal\{N\}C\)\.Nonempty\)𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(interior𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}C𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}apply𝒩\\mathcal\{N\}Set\.Subset\.antisymm𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}closure\_mono𝒩\\mathcal\{N\}\(interior\_subset𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}intro𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rcases𝒩\\mathcal\{N\}hInt𝒩\\mathcal\{N\}with𝒩\\mathcal\{N\}⟨\\langley,𝒩\\mathcal\{N\}hy⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}set𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}𝒩\\mathcal\{N\}×\\times𝒩\\mathcal\{N\}E𝒩\\mathcal\{N\}→\\to𝒩\\mathcal\{N\}E𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}fun𝒩\\mathcal\{N\}p𝒩\\mathcal\{N\}=\>𝒩\\mathcal\{N\}\(1𝒩\\mathcal\{N\}\-𝒩\\mathcal\{N\}p\.1\)𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}p\.1𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}p\.2𝒩\\mathcal\{N\}with𝒩\\mathcal\{N\}hf\_def𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_cont𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}Continuous𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}unfold𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}continuity𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_cont\_at𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ContinuousAt𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}x\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}h\_cont\.continuousAt𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_closure𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}x\)𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(Ioo𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}×\\timess𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[closure\_prod\_eq\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}constructor𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}\(1𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(Ioo𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}1\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[closure\_Ioo𝒩\\mathcal\{N\}\(by𝒩\\mathcal\{N\}norm\_num\)\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}⟨\\langleby𝒩\\mathcal\{N\}norm\_num,𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}norm\_num⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}this𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}hx𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}h\_image𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}’’𝒩\\mathcal\{N\}\(Ioo𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}×\\timess𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}⊆\\subseteq𝒩\\mathcal\{N\}interior𝒩\\mathcal\{N\}C𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rintro𝒩\\mathcal\{N\}\_𝒩\\mathcal\{N\}⟨\\langle⟨\\langleλ\\lambda,𝒩\\mathcal\{N\}w⟩\\rangle,𝒩\\mathcal\{N\}⟨\\langle⟨\\langlehλ\\lambda1,𝒩\\mathcal\{N\}hλ\\lambda2⟩\\rangle,𝒩\\mathcal\{N\}hw⟩\\rangle,𝒩\\mathcal\{N\}rfl⟩\\rangle𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}unfold𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}H𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}λ\\lambda𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}w𝒩\\mathcal\{N\}\+𝒩\\mathcal\{N\}\(1𝒩\\mathcal\{N\}\-𝒩\\mathcal\{N\}λ\\lambda\)𝒩\\mathcal\{N\}⋅\\cdot𝒩\\mathcal\{N\}y𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}interior𝒩\\mathcal\{N\}C𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}hC\.combo\_interior\_self\_subset\_interior𝒩\\mathcal\{N\}hw𝒩\\mathcal\{N\}hy𝒩\\mathcal\{N\}\(by𝒩\\mathcal\{N\}linarith\)𝒩\\mathcal\{N\}\(by𝒩\\mathcal\{N\}linarith\)𝒩\\mathcal\{N\}\(by𝒩\\mathcal\{N\}ring\)𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}simpa𝒩\\mathcal\{N\}\[add\_comm\]𝒩\\mathcal\{N\}using𝒩\\mathcal\{N\}H𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}H1𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}x\)𝒩\\mathcal\{N\}∈\\in𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(f𝒩\\mathcal\{N\}’’𝒩\\mathcal\{N\}\(Ioo𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}×\\timess𝒩\\mathcal\{N\}C\)\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}h\_cont\_at\.mem\_closure\_image𝒩\\mathcal\{N\}h\_closure𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}H2𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(f𝒩\\mathcal\{N\}’’𝒩\\mathcal\{N\}\(Ioo𝒩\\mathcal\{N\}\(0𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}ℝ\\mathbb\{R\}\)𝒩\\mathcal\{N\}1𝒩\\mathcal\{N\}×\\timess𝒩\\mathcal\{N\}C\)\)𝒩\\mathcal\{N\}⊆\\subseteq𝒩\\mathcal\{N\}closure𝒩\\mathcal\{N\}\(interior𝒩\\mathcal\{N\}C\)𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}closure\_mono𝒩\\mathcal\{N\}h\_image𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}have𝒩\\mathcal\{N\}:𝒩\\mathcal\{N\}f𝒩\\mathcal\{N\}\(1,𝒩\\mathcal\{N\}x\)𝒩\\mathcal\{N\}=𝒩\\mathcal\{N\}x𝒩\\mathcal\{N\}:=𝒩\\mathcal\{N\}by𝒩\\mathcal\{N\}simp𝒩\\mathcal\{N\}\[f\]𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}rw𝒩\\mathcal\{N\}\[this\]𝒩\\mathcal\{N\}at𝒩\\mathcal\{N\}H1𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}𝒩\\mathcal\{N\}exact𝒩\\mathcal\{N\}H2𝒩\\mathcal\{N\}H1Analysis:This proof suffers from an Illegal Identifier syntax error\. In the destructuring steprintro \_⟨⟨λ\\langle\\langle\\lambda, w⟩⟩\\rangle\\rangle, \.\.\., the model attempts to bind a real number to the variable nameλ\\lambda\. However,λ\\lambda\(\\lambda\) is a strictly reserved system keyword in Lean \(utilized for lambda abstractions or anonymous functions\)\. Utilizing it as a local variable identifier violates Lean 4 lexical rules and immediately breaks the parser\.

## Appendix CPrompts

Prompt for Goedel\-Prover\-V2 and DeepSeek\-Prover\-V2\\KV@do,breaklines=true, breakanywhere=true,,Complete the following Lean 4 code:\`\`\`lean4\{formal\_statement\}\`\`\`Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies\.The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof\.

Prompt for Kimina\-Prover\\KV@do,breaklines=true, breakanywhere=true,,You are an expert in mathematics and proving theorems in Lean 4\. Think about and solve the following problem step by step in Lean 4\.Problem:\{informal\_statement\}Formal statement:\`\`\`lean4\{formal\_statement\}\`\`\`

Prompt for General\-Purpose Models\\KV@do,breaklines=true, breakanywhere=true,,You are an expert in Lean 4 and Mathematics\. Please finish the following proof in Lean4 code\.Do not change the original statement\. Copy the final statement to prove exactly\.Please include the complete header \(including imports and namespaces\) so that your code can pass the Lean4 compiler\. Please solve the statement step by step and provide your complete Lean4 code between \`\`\`lean4 and \`\`\` after careful reasoning\.The statement for you to complete is:\`\`\`lean4\{formal\_statement\}\`\`\`

Prompt for GPT\-5\.5 Informal Proof Grading\\KV@do,breaklines=true, breakanywhere=true,,\#\# InstructionYour task is to evaluate the quality of a solution to a problem\. The problem may ask for a proof of statement, or ask for an answer\. If finding an answer is required, the solution should present the answer, and it should also be a rigorous proof of that answer being valid\.Please evaluate the solution and score it according to the following criteria:\- If the solution is completely correct, with all steps executed properly and clearly demonstrated, then the score is 1\- If the solution is generally correct, but with some details omitted or minor errors, then the score is 0\.5\- If the solution does not actually address the required problem, contains fatal errors, or has severe omissions, then the score is 0\- Additionally, referencing anything from any paper does not save the need to prove the reference\. It’s okay IF AND ONLY IF the solution also presents a valid proof of the reference argument\(s\); otherwise, if the solution omits the proof or if the proof provided is not completely correct, the solution should be scored according to the criteria above, and definitely not with a score of 1Please carefully reason out and analyze the quality of the solution below, and in your final response present a detailed evaluation of the solution’s quality followed by your score\. Therefore, your response should be in the following format:Here is my evaluation of the solution:\.\.\. // Your evaluation here\. You are required to present in detail the key steps of the solution or the steps for which you had doubts regarding their correctness, and explicitly analyze whether each step is accurate: for correct steps, explain why you initially doubted their correctness and why they are indeed correct; for erroneous steps, explain the reason for the error and the impact of that error on the solution\.Based on my evaluation, the final overall score should be:\\boxed\{\.\.\.\} // where \.\.\. should be the final overall score \(0, 0\.5, or 1, and nothing else\) based on the above criteria\-\-\-Here is your task input:\#\# Problem\{statement\}\#\# Solution\{proof\}