Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

# Dataset Defects and Evaluation Failures in Lean Theorem Proving
Source: [https://arxiv.org/html/2606.29493](https://arxiv.org/html/2606.29493)
## Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

###### Abstract

Benchmarks for LLM\-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine\-checked proof\. However, the kernel only checks that a proof establishes a*formal*statement; it does not verify that the statement faithfully encodes the intended informal problem, nor that evaluation harnesses are robust to trivial or adversarial solutions\. We audit five widely used Lean theorem\-proving benchmarks and their forks, using corpus\-scale static checkers to surface 4,833 findings, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms\. We also document semantic defects such as missing hypotheses, problem simplification, incomplete or incorrect translations, and Lean\-specific specification hazards\. Beyond dataset construction, we survey evaluation\-time failure modes and show, on corrected subsets, that defects can both inflate and deflate reported prover scores\. We propose a fault taxonomy, a suite of automated checkers and recall\-oriented semantic\-audit prompts, and release standards to guide the creation of formal math datasets and make evaluation more reproducible and trustworthy\. Our checkers, audit prompts, and corrected dataset snapshots are available at[https://github\.com/Shashi456/atp\-checkers](https://github.com/Shashi456/atp-checkers)\.

Automated theorem proving, Formal math

## 1Introduction

Deep learning has rapidly advanced automated theorem proving, with models increasingly trained to produce proofs in Lean\. Recent systems such as DeepSeek\-Prover V2\(Renet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib27)\), Goedel Prover 2\(Linet al\.,[2026](https://arxiv.org/html/2606.29493#bib.bib34)\), and Kimina Prover\(Wanget al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib28)\)report progress on widely used benchmarks such as miniF2F and ProofNet\. However, as in other LLM evaluation settings, benchmark scores can be misleading when problem statements are mis\-specified or become outdated, or when evaluation protocols contain loopholes\.

A common intuition is that Lean benchmarks are “self\-verifying” because the kernel checks every proof\. This intuition is incomplete\. The Lean kernel provides certainty about a narrow claim: a given proof artifact establishes a given*formal statement*\. This provides mathematical certainty about the formal claim, but overall benchmark reliability is limited by specification accuracy and by the correctness of the natural\-language\-to\-Lean translation\. Lean does not certify that the formal statement matches the intended informal problem, that the benchmark avoids Lean\-specific semantic pitfalls, or that the evaluation protocol cannot be exploited\. These gaps can inflate reported success without demonstrating stronger proof capability\.

Table 1:Benchmarks referenced in this study \(details in §3\)\.![Refer to caption](https://arxiv.org/html/2606.29493v1/benchmark_stack3.png)Figure 1:The formal benchmarking pipeline and where errors can enter\. The kernel \(trust boundary\) certifies only that a proof artifact establishes the*formal*Lean statement\. Three categories of issues arise:Fidelity Issuesin the translation step,Evaluation Loopholes\(robustness\) in the proof\-checking and reporting steps, andMaintenance Issues\(validity \+ drift\) spanning the entire pipeline\. Table[2](https://arxiv.org/html/2606.29493#S2.T2)details the specific fault types within each category\.In this paper, we audit five widely used Lean benchmarks and their forks \([Table1](https://arxiv.org/html/2606.29493#S1.T1)\)\. We analyze the benchmark development pipeline \([Section2](https://arxiv.org/html/2606.29493#S2)\) and develop a fault taxonomy \([Section3](https://arxiv.org/html/2606.29493#S3)\) that separates formalization\-time fidelity failures, evaluation\-time loopholes, and maintenance decay\. To scale detection beyond manual review, we implement automated static checkers as Lean 4 metaprograms and run them corpus\-wide across all 13 benchmark variants \(∼10,000\{\\sim\}10\{,\}000problems\), surfacing 4,833 findings of which 398 carry a machine\-checkable certificate of unprovability or vacuity; we additionally evaluate LLM\-based prompts on a labeled 92\-problem challenge set for the semantic mismatches static analysis cannot decide, and measure how corrected statements change reported prover scores \([Section4](https://arxiv.org/html/2606.29493#S4)\)\. Finally, we propose release standards and tooling to harden future dataset creation and evaluation \([Section5](https://arxiv.org/html/2606.29493#S5)\)\.

## 2What Formal Benchmarking Certifies \(and What It Does Not\)

Formal benchmarks are typically adapted from informal problems through a series of steps that can undermine the validity of the benchmark\. Figure[1](https://arxiv.org/html/2606.29493#S1.F1)illustrates this pipeline\. We walk through each stage below, noting where errors can enter the pipeline\.

##### Step 1: Informal Problem\.

The pipeline begins with aninformal problem, an Olympiad question, textbook exercise, or research conjecture stated in natural language\. Issues can already arise at this stage: the source material may contain errors, the problem may be ill\-posed or ambiguous, the mathematical claim may be false\. These are*validity*issues that no amount of careful formalization can fix\.

##### Step 2: Formalization\.

The informal problem is thenformalizedinto a Lean statement\. This translation step is where most defects arise \(*fidelity*issues\)\. Hypotheses can be omitted, domains mistranslated \(e\.g\.,ℕ\\mathbb\{N\}instead ofℤ\\mathbb\{Z\}\), or Lean\-specific encoding issues can silently change meaning or make a theorem vacuous\. A proof of the resulting formal statement may be mathematically valid yet prove something different from what the informal problem intended\.

##### Step 3: Model/Prover\.

A model or automated prover receives the Lean statement \(plus a prompt and policy\) and attempts to produce aproof artifact\.

##### Step 4: Lean Kernel\.

The proof artifact is checked by the Lean kernel, which emits a pass/fail result\. This is thetrust boundary: the kernel provides mathematical certainty that the proof artifact establishes the formal statement\. However, models can find bugs in the Lean environment thus producing proofs that appear to be “accepted” without proper kernel verification \(*robustness*issues\)\.

##### Step 5: Reported Metric\.

Finally, the evaluation harness aggregates pass/fail results into a reported metric\. Loopholes at the previous stage can inflate scores without demonstrating genuine capability\.

##### What the kernel certifies\.

The key insight is that Lean’s kernel, the only component providing mathematical certainty, operates at a single point in this pipeline\. The trust boundary in Figure[1](https://arxiv.org/html/2606.29493#S1.F1)marks the limit of what Lean guarantees: everything to the left of the kernel and everything to the right must be validated by other means\. It does*not*certify that the formal statement matches the intended informal problem \(Step 2\), nor that the informal problem itself is correct \(Step 1\), nor that the evaluation protocol and metric reporting are sound \(Step 5\)\.

Table 2:Taxonomy of faults in Lean theorem proving benchmarks\.CategorySubcategoryIssuesFidelitySpecificationMissing hypotheses/conditions; extra or incorrect constraints; incomplete or oversimplified specFormalizationGoal/premise translation errors; missing subgoals; vacuous hypothesesDomain & DefinitionWrong type; wrong mathlib concept; misuse of library API; encoding artifactsLean EncodingNat subtraction truncation; division/mod by zero; Int/Nat coercionEvaluation
\(robustness\)Proof AcceptanceImproper axiom usage;native\_decideshortcuts; unsafe tacticsMaintenance
\(validity \+ drift\)DecayVersion drift \(Lean 3→\\rightarrow4\); dependency rot \(mathlib API changes\)Benchmark DefectsNL statement defects; unprovable statements; harness driftWe organize these failure modes into three categories \(Figure[1](https://arxiv.org/html/2606.29493#S1.F1), bottom; Table[2](https://arxiv.org/html/2606.29493#S2.T2)\):Fidelity Issuesarise in Step 2;Evaluation Loopholesarise in Steps 4–5;Maintenance Issuesspan the entire pipeline, including source errors in Step 1 and semantic drift as mathlib evolves over time\.

## 3Fault Taxonomy and Representative Failures

Our audit of miniF2F, ProofNet, FormalMath, CombiBench, and ProverBench revealed that benchmark defects cluster into categories requiring fundamentally different interventions\. We organize faults by where they enter the benchmarking pipeline \(Figure[1](https://arxiv.org/html/2606.29493#S1.F1)\) and what fix they require \(Table[2](https://arxiv.org/html/2606.29493#S2.T2)\):

- •Fidelity issues: issues during formalization require careful review at creation time/ lean encoding hazards can be detected by static analysis
- •Evaluation loopholes: require stricter harnesses and patched Lean versions
- •Maintenance decay: requires version pinning and active stewardship

One cannot “fix” a kernel bug/bypass by adding dataset review, nor prevent missing hypotheses by restricting tactics\. The taxonomy makes remediation actionable by matching faults to appropriate interventions\. We illustrate each category with representative defects from our audit and tag every example with its \(sub\)category; further examples appear in Appendix[B](https://arxiv.org/html/2606.29493#A2)\.

### 3\.1Fidelity Issues

These faults occur when the Lean statement does not faithfully encode the intended informal problem\. We distinguish two primary failure modes:\.*Specification errors*omit required content, such as missing hypotheses, dropped subgoals, or unencoded constraints, leaving the statement valid but*weaker*than intended, and therefore easier to prove than the original\.*Formalization errors*instead misrepresent the original, through incorrect translation, wrong quantifier scope, or encoding artifacts, so the statement may become*unprovable*or prove*something different*\. The two demand opposite repairs: a specification error is fixed by*adding*the missing content, a formalization error by*correcting*the encoding\.

##### Missing hypotheses\.

\(Specification\)Forgetting properties of mathematical objects can make problems trivial, vacuous, or false\. In[Figure2](https://arxiv.org/html/2606.29493#S3.F2), the formalization omits the requirement thatVVbe finite\-dimensional, a hypothesis explicitly stated in the informal problem and essential for the result\.

ProofNet – Axler Exercise 3\.8Problem:Suppose thatVVisfinite dimensionaland thatT∈ℒ​\(V,W\)T\\in\\mathcal\{L\}\(V,W\)\. Prove that there exists a subspaceUUofVVsuch thatU∩null​T=\{0\}U\\cap\\text\{null \}T=\\\{0\\\}and rangeT=\{T​u:u∈U\}T=\\\{Tu:u\\in U\\\}\.[⬇](data:text/plain;base64,dGhlb3JlbSBleGVyY2lzZV8zXzgge0YgViBXIDogVHlwZSp9IFthZGRfY29tbV9ncm91cCBWXQogIFthZGRfY29tbV9ncm91cCBXXSBbZmllbGQgRl0gW21vZHVsZSBGIFZdIFttb2R1bGUgRiBXXQogIChMIDogViDihpLigpdbRl0gVykgOgogIOKIgyBVIDogc3VibW9kdWxlIEYgViwgVSDiipMgTC5rZXIgPSDiiqUg4oinCiAgICBsaW5lYXJfbWFwLnJhbmdlIEwgPSByYW5nZSAoZG9tX3Jlc3RyaWN0IEwgVSkgOj0gc29ycnk=)theorem𝒫\\mathscr\{P\}exercise\_3\_8𝒫\\mathscr\{P\}\{F𝒫\\mathscr\{P\}V𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Type\*\}𝒫\\mathscr\{P\}\[add\_comm\_group𝒫\\mathscr\{P\}V\]𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\[add\_comm\_group𝒫\\mathscr\{P\}W\]𝒫\\mathscr\{P\}\[field𝒫\\mathscr\{P\}F\]𝒫\\mathscr\{P\}\[module𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}V\]𝒫\\mathscr\{P\}\[module𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}W\]𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(L𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}V𝒫\\mathscr\{P\}→\\rightarrowl\[F\]𝒫\\mathscr\{P\}W\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}U𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}submodule𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}V,𝒫\\mathscr\{P\}U𝒫\\mathscr\{P\}⊓\\sqcap𝒫\\mathscr\{P\}L\.ker𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}⊥\\bot𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}linear\_map\.range𝒫\\mathscr\{P\}L𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}range𝒫\\mathscr\{P\}\(dom\_restrict𝒫\\mathscr\{P\}L𝒫\\mathscr\{P\}U\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}sorryFigure 2:Missing hypothesis: the Lean statement omits finite\-dimensionality, which is required for the theorem to hold\.
##### Incomplete translation\.

\(Formalization\)Problems often have several parts, and a formalization can silently drop one\. In[Figure3](https://arxiv.org/html/2606.29493#S3.F3), the Lean statement captures the inequality but omits the “determine when equality occurs” requirement, encoding only half of the intended problem and leaving it strictly weaker than the original\. In another example[Figure5](https://arxiv.org/html/2606.29493#S3.F5), the formalization leavesuuas a free variable without specifyingu=y−2​xu=y\-2x\.

miniF2F – IMO 1983 Problem 6Problem:Letaa,bbandccbe the lengths of the sides of a triangle\. Prove thata2​b​\(a−b\)\+b2​c​\(b−c\)\+c2​a​\(c−a\)≥0a^\{2\}b\(a\-b\)\+b^\{2\}c\(b\-c\)\+c^\{2\}a\(c\-a\)\\geq 0\.Determine when equality occurs\.[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9fMTk4M19wNiAoYSBiIGMgOiDihJ0pICho4oKAIDogMCA8IGEg4oinIDAgPCBiIOKIpyAwIDwgYykKICAoaOKCgSA6IGMgPCBhICsgYikgKGjigoIgOiBiIDwgYSArIGMpICho4oKDIDogYSA8IGIgKyBjKSA6CiAgMCDiiaQgYV4yICogYiAqIChhIC0gYikgKyBiXjIgKiBjICogKGIgLSBjKSArCiAgICAgIGNeMiAqIGEgKiAoYyAtIGEpIDo9IHNvcnJ5)theorem𝒫\\mathscr\{P\}imo\_1983\_p6𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}\(h3𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}a^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(b𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}c^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(c𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}a\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}sorryFigure 3:Incomplete specification: the equality\-case determination is missing from the formalization\.
##### Wrong domain or type\.

\(Domain & Definition mismatch\)Translating variable domains inaccurately changes problem semantics\. If a problem states “for all positive integersnn,” using\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)without a guard\(hn𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}n\)includesn=0n=0\. Conversely, usingℕ\\mathbb\{N\}whenℤ\\mathbb\{Z\}is intended can introduce truncation errors\.

##### Nat subtraction and division hazards\.

\(Lean Encoding\)Even when a statement “looks correct,” Lean semantics can silently change meaning: We found multiple instances in FormalMath and ProverBench whereℕ\\mathbb\{N\}subtraction silently changed problem semantics \(Appendix[B](https://arxiv.org/html/2606.29493#A2)\)\.

##### Definition mismatch\.

\(Domain & Definition mismatch\)Sometimes the Lean encoding uses an incorrect or outdated mathlib concept\. This is a mathematical representation issue\.

##### Vacuous hypotheses\.

\(Formalization\)Incorrect translation can produce contradictory hypotheses, making statements vacuously true\. For example, an earlier CombiBench formalization encoded a minimality condition as∀N′<N,¬Periodic​\(W,N′\)\\forall N^\{\\prime\}<N,\\,\\neg\\texttt\{Periodic\}\(W,N^\{\\prime\}\), butPeriodic W 0is trivially provable in lean withsimp\. This made the hypotheses unsatisfiable, allowing a trivialexfalsoproof \(Appendix[E](https://arxiv.org/html/2606.29493#A5)\)\.

### 3\.2Evaluation loopholes

Even if the benchmark statement is correct, an evaluation can be invalidated when the harness accepts a proof artifact that does not demonstrate the intended capability\.

##### Theapply?frontend bug\.

A bug in Lean versions prior to 4\.20\.0 allowed theapply?tactic to report success without producing a theorem declaration that had passed ordinary kernel verification: a synthetic sorry interacted with a universe\-level mismatch and bypassed the usual “declaration uses sorry” warning\. This failure mode appeared in at least three proofs claimed by DeepSeek\-Prover\-V2\(Renet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib27)\): one miniF2F solution and two PutnamBench solutions from the 7B model \(Appendix[D](https://arxiv.org/html/2606.29493#A4)\)\. The bug has since been fixed,111[https://github\.com/leanprover/lean4/pull/8231](https://github.com/leanprover/lean4/pull/8231)but it illustrates a broader concern:*RL\-trained provers will find and exploit any verification loophole that increases reward*\.

The Lean community has since releasedcomparator,222[https://github\.com/leanprover/comparator](https://github.com/leanprover/comparator)a trusted evaluator that checks proofs against a conservative set of axioms and disallows potentially unsafe tactics likenative\_decide\. Whilecomparatordoes not address all end\-to\-end trustworthiness issues \(e\.g\. theapply?bug, which operated below the tactic layer\), it represents an important step toward trustworthy evaluation\. We recommend that evaluation harnesses use patched Lean versions, verify\#print axiomsoutput, and incorporate maximally strict verification in RL reward signals\.

##### Native\_decide trust expansion

native\_decideexpands the trusted computing base beyond the kernel by trusting the compiler/codegen result via theLean\.ofReduceBoolaxiom\. This expands the trusted code base from the kernel to the entire compiler: known bugs in native code generation and implemented\_by overrides have produced proofs of False\. Evaluation harnesses should disallownative\_decideor carefully restrict its use\.

##### Axiom injection\.

If the environment containsaxiom​h:P\\texttt\{axiom\}~h:P, then any solver can “prove”PPby citinghh\. Benchmark harnesses should forbid axioms in problem files and in any imported modules\.

##### Over\-permissive tactics and unsafe automation\.

Tactics likedecidecan solve goals by computation when that is intended, but they can also collapse tasks when the goal is improperly typed or overly concrete\. A robust harness should specify which tactics are allowed and record the exact proof artifact\.

### 3\.3Maintenance & Source Issues

Even a faithful, well\-evaluated benchmark degrades over time\. Lean and mathlib evolve rapidly; benchmarks released against a specific snapshot can stop compiling within months, and quick fixes can introduce semantic drift\. Some problems are defective at the source \(ambiguous, ill\-posed, or false NL statements\)\. Others become defective through*harness drift*: inconsistent versioning updates and unrecorded benchmark changes, across evaluation setups, make reproducibility unreliable\.

##### Version drift\.

\(Maintenance Decay\)The Lean theorem prover\(de Mouraet al\.,[2015](https://arxiv.org/html/2606.29493#bib.bib35)\)evolves rapidly, with new tactics and library conventions shipping in successive releases\. Lean 4’s first stable release was on September 8, 2023, and new versions arrive within months; a benchmark pinned to one Lean/mathlib snapshot can fail to compile as APIs change, or shift in meaning as definitions are revised\. For example, when ProofNet was first released the mathlib predicatePerfectdid not yet exist, so the authors encoded a perfect set as one that is closed \(IsClosed\) and equal to its set of cluster points \([Figure4](https://arxiv.org/html/2606.29493#S3.F4)\)\. The later ProofNet\# version uses mathlib’sPerfectpredicate, which exposes a much larger API and changes the nature of the mechanization\. In paper mathematics the two encodings are interchangeable, and a mathematician would move freely between them; in a mechanized setting that flexibility is not free, and substituting one for the other requires first proving their equivalence\.

Problem StatementRudin Ex\. 2\.28:Prove that every closed set in a separable metric space is the union of a \(possibly empty\) perfect set and a set which is at most countable\.

ProofNet \(Incomplete\)[⬇](data:text/plain;base64,dGhlb3JlbSBleGVyY2lzZV8yXzI4IChYIDogVHlwZSopCiAgW21ldHJpY19zcGFjZSBYXSBbc2VwYXJhYmxlX3NwYWNlIFhdCiAgKEEgOiBTZXQgWCkgKGhBIDogaXNfY2xvc2VkIEEpIDoKICDiiIMgUOKCgSBQ4oKCIDogU2V0IFgsIEEgPSBQ4oKBIOKIqiBQ4oKCIOKIpwogICAgaXNfY2xvc2VkIFDigoEg4oinCiAgICBQ4oKBID0ge3ggfCBjbHVzdGVyX3B0IHggICjihJkgUOKCgSkgfSDiiKcgc2V0LmNvdW50YWJsZSBQ4oKCIDo9IHNvcnJ5)theorem𝒫\\mathscr\{P\}exercise\_2\_28𝒫\\mathscr\{P\}\(X𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Type\*\)𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\[metric\_space𝒫\\mathscr\{P\}X\]𝒫\\mathscr\{P\}\[separable\_space𝒫\\mathscr\{P\}X\]𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(A𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Set𝒫\\mathscr\{P\}X\)𝒫\\mathscr\{P\}\(hA𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}is\_closed𝒫\\mathscr\{P\}A\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Set𝒫\\mathscr\{P\}X,𝒫\\mathscr\{P\}A𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}∪\\cup𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}is\_closed𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}\{x𝒫\\mathscr\{P\}\|𝒫\\mathscr\{P\}cluster\_pt𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(ℙ\\mathbb\{P\}𝒫\\mathscr\{P\}P1\)𝒫\\mathscr\{P\}\}𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}set\.countable𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}sorry

ProofNet\# \(Correct\)[⬇](data:text/plain;base64,dGhlb3JlbSBleGVyY2lzZV8yXzI4IChYIDogVHlwZSopCiAgW01ldHJpY1NwYWNlIFhdIFtTZXBhcmFibGVTcGFjZSBYXQogIChBIDogU2V0IFgpIChoQSA6IElzQ2xvc2VkIEEpIDoKICDiiIMgUOKCgSBQ4oKCIDogc2V0IFgsIEEgPSBQ4oKBIOKIqiBQ4oKCIOKIpwogICAgUGVyZmVjdCBQ4oKBIOKIpwogICAgU2V0LkNvdW50YWJsZSBQ4oKCIDo9IHNvcnJ5)theorem𝒫\\mathscr\{P\}exercise\_2\_28𝒫\\mathscr\{P\}\(X𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Type\*\)𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\[MetricSpace𝒫\\mathscr\{P\}X\]𝒫\\mathscr\{P\}\[SeparableSpace𝒫\\mathscr\{P\}X\]𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(A𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Set𝒫\\mathscr\{P\}X\)𝒫\\mathscr\{P\}\(hA𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}IsClosed𝒫\\mathscr\{P\}A\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}set𝒫\\mathscr\{P\}X,𝒫\\mathscr\{P\}A𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}∪\\cup𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Perfect𝒫\\mathscr\{P\}P1𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Set\.Countable𝒫\\mathscr\{P\}P2𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}sorry

Figure 4:Version and definition drift: the original ProofNet version encodes “perfect set” using closure and cluster points; the later version uses mathlib’sPerfectpredicate\.A similar difference between paper\-and\-pen mathematics and formal mathematics is that of limits\. Limits in mathlib are defined using filters333[https://Leanprover\-community\.github\.io/mathlib4\_docs/Mathlib/Topology/Defs/Filter\.html](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Defs/Filter.html)rather than the usualϵ−δ\\epsilon\-\\deltadefinition, since filters unify the disparate conditions needed to define two\-sided limits, one\-sided limits, and limits to±∞\\pm\\infty\. Another example is that of a semilinear map\(Dupuiset al\.,[2024](https://arxiv.org/html/2606.29493#bib.bib12)\), which is a generalization of linear maps, created to unify linear algebra overℝ\\mathbb\{R\}andℂ\\mathbb\{C\}, whereℂ\\mathbb\{C\}has an extra complex\-conjugate structure\. These examples are not exhaustive; mathlib evolves daily, and it is a challenge to keep datasets up\-to\-date with emerging best practices and API\.

##### Fork proliferation\.

\(Maintenance Decay\)Version drift cascades into fork proliferation, in which multiple ports of one dataset coexist with inconsistent splits, undocumented corrections, and unclear lineage\. For miniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2606.29493#bib.bib22)\)alone, widely used variants include the original release,444[https://github\.com/openai/miniF2F](https://github.com/openai/miniF2F)the Draft, Sketch, and Prove version\(Jianget al\.,[2023](https://arxiv.org/html/2606.29493#bib.bib8)\),555[https://github\.com/facebookresearch/miniF2F](https://github.com/facebookresearch/miniF2F)a Lean 4 port maintained by Kaiyu Yang,666[https://github\.com/yangky11/miniF2F\-lean4/tree/main](https://github.com/yangky11/miniF2F-lean4/tree/main)the Kimina\-Prover version\(Wanget al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib28)\),777[https://huggingface\.co/datasets/AI\-MO/miniF2F\_test](https://huggingface.co/datasets/AI-MO/miniF2F_test)and a version introduced by Harmonic\([harmonic Community,](https://arxiv.org/html/2606.29493#bib.bib30)\)\.888[https://github\.com/Harmonic\-ai/datasets](https://github.com/Harmonic-ai/datasets)Papers often do not specify which version they used, making cross\-paper comparisons unreliable\.

##### NL statement defect\.

\(Benchmark Defects\)Some problems are defective before any formalization occurs\. A ProverBench problem \([Figure5](https://arxiv.org/html/2606.29493#S3.F5)\) states that the general solution tox2\+y2−1=4​x​yx^\{2\}\+y^\{2\}\-1=4xyisx\+u​3=\(2\+3\)nx\+u\\sqrt\{3\}=\(2\+\\sqrt\{3\}\)^\{n\}, whereas the correct Pell reduction givesu\+x​3=\(2\+3\)nu\+x\\sqrt\{3\}=\(2\+\\sqrt\{3\}\)^\{n\}, with the variables swapped\. No amount of better Lean encoding can repair a wrong source problem; these defects require checking the mathematics itself\.

Number Theory P2: ProverBenchProblem:For the equationx2\+y2−1=4​x​yx^\{2\}\+y^\{2\}\-1=4xyits general solution in the integers is given byx\+u​3=\(2\+3\)nx\+u\\sqrt\{3\}=\(2\+\\sqrt\{3\}\)^\{n\}, whereuuis the substitute fory−2​xy\-2x\.[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gZ2VuZXJhbF9zb2x1dGlvbl9xdWFkcmF0aWNfZXF1YXRpb24gKHggeSA6IOKEpCkgKHUgOiDihKQpIChuIDog4oSVKSA6CiAgeF4yICsgeV4yIC0gMSA9IDQgKiB4ICogeSDihpIgeCArIHUgKiBSZWFsLnNxcnQgMyA9ICgyICsgUmVhbC5zcXJ0IDMpXm4gOj0KICBzb3JyeQ==)import𝒫\\mathscr\{P\}Mathlibtheorem𝒫\\mathscr\{P\}general\_solution\_quadratic\_equation𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}\)𝒫\\mathscr\{P\}\(u𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}\)𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}x^2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}y^2𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}u𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}\(2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}3\)^n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorryFigure 5:Incorrect source statement: the correct Pell reduction givesu\+x​3=\(2\+3\)nu\+x\\sqrt\{3\}=\(2\+\\sqrt\{3\}\)^\{n\}\.

## 4Automated Checkers

We develop both static analyzers for mechanical hazards and LLM\-based detectors for semantic mismatches\. The two approaches are complementary: static checkers are cheap and deterministic but cannot assess whether a formalization captures mathematical intent; LLMs can reason about semantics but require human verification\.

### 4\.1Static Checkers

We implement static analyzers as Lean 4 metaprograms\(Paulinoet al\.,[2024](https://arxiv.org/html/2606.29493#bib.bib36)\)that detect common formalization pitfalls\. Our approach combines syntactic pattern matching with semantic guard proving: when a potentially problematic pattern is detected, we attempt to discharge the necessary guard condition using tactics likeomega,assumption, andsimp\. A finding is reported only when the guard cannot be automatically proven\. These serve as the equivalent to unit tests for Lean statements\.

Table[3](https://arxiv.org/html/2606.29493#S4.T3)summarizes our checkers, ordered by severity\. The first three checkers target*soundness failures*: specifications that are provably wrong or vacuously true\. The remaining checkers target issues arising from Lean’s totalized arithmetic, where division by zero returns zero \(2/0=02/0=0\), imaginary components are converted to zero \(−1=0\\sqrt\{\-1\}=0\), and natural subtraction truncates \(2−3=02\-3=0\)\. Full descriptions appear in Appendix[F](https://arxiv.org/html/2606.29493#A6)\.

Table 3:Automated checkers ordered by severity\. Checkers marked with†\\daggersupport LLM\-assisted false positive filtering\.Table 4:Static\-checker findings across all five benchmarks and their1313released variants \(∼\\sim10,000 problems; forks, ports, and splits are counted separately and not deduplicated\)\.Find\.: total audit signals\.Proven: findings carrying a machine\-checkable certificate of unprovability or vacuity\. The category columns give the dominant hazard classes \(Div/0,Nat Sub,Int Div, andAnalyticare arithmetic/domain totalizations;AxiomandCExare soundness failures\); because a statement may trigger several checkers and a few smaller categories are omitted, the category columns need not sum toFind\.orProven\. Upstream sources for every variant are given in[Table8](https://arxiv.org/html/2606.29493#A1.T8)\([SectionA\.2](https://arxiv.org/html/2606.29493#A1.SS2)\)\.##### Corpus\-scale audit results\.

Running the static checkers over all released variants surfaces 4,833 findings and 399 proven issues \([Table4](https://arxiv.org/html/2606.29493#S4.T4)\)\. These counts should not be read as deduplicated benchmark\-level error rates: several rows are forks, ports, or subsets of the same underlying benchmark\. They instead show that the audit is corpus\-wide, while semantic equivalence still requires human adjudication\.

##### LLM\-assisted false positive filtering\.

Static analysis produces false positives when guards exist in forms the prover cannot recognize, for example, guards embedded in structure definitions, subtype constraints like\{x:ℝ//0<x\}\\\{x:\\mathbb\{R\}//0<x\\\}, or non\-local invariants\. For findings in the†\\dagger\-marked categories, we employ a secondary LLM verification stage that examines the surrounding code context to determine whether a semantic guard exists\.

The authors labeled a 55\-example ProverBench warning\-verification set spanning division by zero, Nat subtraction, analytic\-domain, and modulo warnings \(Table[5](https://arxiv.org/html/2606.29493#S4.T5)\)\. Gemini 3\.0 Flash achieves the highest accuracy \(83\.3%\) at lowest cost\. On ProverBench, LLM filtering reduces findings from 427 to 277 \(35% reduction\) while preserving all confirmed true positives\. We conclude that although static checkers \+ LLM assisted filtering is not totally foolproof, they often successfully surface statements that are worth taking another look at\.

Table 5:LLM verification performance for filtering static checker false positives\.

### 4\.2LLM\-Assisted Semantic Audit

While static checkers detect syntactic hazards, they cannot identify*semantic*mismatches between informal problems and their formal translations—missing hypotheses, incorrect domains, or definition mismatches\. We evaluate whether LLMs can reliably detect such errors when prompted with our fault taxonomy\.

##### Detection framework\.

For each benchmark problem, we present the LLM with the informal problem statement, the formal Lean statement, a description of one error category, and few\-shot examples\. The model outputs whether the specified error type is present\. We evaluate six categories aligned with Table[2](https://arxiv.org/html/2606.29493#S2.T2): problem statement errors, specification errors, formalization errors, domain mismatches, definition mismatches, and quantifier/indexing mismatches\.

##### Evaluation\.

We evaluate on a curated 92\-problem challenge set across FormalMath \(22\), ProofNet \(13\), ProverBench \(23\), and CombiBench \(34\), with each problem assessed across all six categories \(552 total classifications\)\. This set is not used to estimate benchmark\-level prevalence\. It is sourced from set of NL/Lean pairs for which we had ground\-truth labels from community reports of various datasets like FormalMath and Proverbench, ProofNet/ProofNet\# comparison, and Combibench diffs; unequal per\-benchmark counts reflect where labeled errors were available\.

Table 6:LLM\-assisted semantic audit: Models achieve high recall for detecting formalization errors but require human filtering of false positives\.Both models reach high recall but low precision overall \([Table6](https://arxiv.org/html/2606.29493#S4.T6)\), and performance varies substantially by error type \([Table7](https://arxiv.org/html/2606.29493#S4.T7)\): they detectspecification errorsanddefinition mismatches, where the discrepancy is often explicit, far more reliably thanformalization errors, which require deeper semantic understanding of whether the Lean encoding preserves mathematical intent\.

Table 7:Per\-type F1 scores for semantic error detection\.
##### Practical workflow\.

We recommend a two\-stage pipeline: \(1\) run static checkers to flag syntactic hazards cheaply and deterministically, then \(2\) apply LLM\-based semantic review as a high\-recall screen for problems that require semantic judgment\. LLM\-assisted audit can identify the∼80%\{\\sim\}80\\%of problems likely to contain errors, allowing human experts to focus verification effort on flagged items\. Human review remains the gold standard for final adjudication\. Full per\-dataset results and prompt details appear in Appendix[H](https://arxiv.org/html/2606.29493#A8)\.

### 4\.3Effect on Reported Prover Scores

Defects matter for evaluation as they change reported numbers, and they can do so in two opposing ways\. As a direct check, we selected 20 problems with mechanically proven issues across four datasets, manually corrected the statements, and evaluated provers on the original and corrected versions\. The original flawed statements were unprovable, and both evaluated models solved 0/20; after correction, DeepSeek\-Prover\-V2\-7B solved 3/20 and Kimina\-Prover\-8B solved 2/20\. Such items do not make a benchmark easier; they silently*deflate*scores by adding impossible problems to the denominator\.

The opposite failure mode also occurs: a formalization*weaker*than the informal problem is easier to prove and*inflates*scores\. Consistent with this, repairing the weakened statements that distinguish ProofNet from its human\-corrected counterpart ProofNet\#\(Poirouxet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib44)\)lowers measured pass rates for the provers we tested\. Because the two effects pull in opposite directions, they can coexist within a single benchmark and partially cancel, leaving headline pass rates unreliable without a per\-item dataset\-quality audit\.

## 5Lessons Learned: Release Standards for Trustworthy Benchmarks

We propose release standards that are cheap to adopt and prevent common failure modes:

Useproof\_wantedfor problem statements\.Lean’ssorrytactic is widely used as a placeholder during benchmark creation, but it has a critical side effect:sorryadds the statement to the environment as an axiom, meaning any downstream code can reference it as a proven fact\. An RL\-trained prover can exploit this by citing the sorry\-admitted statement rather than constructing a genuine proof\. Theproof\_wantedkeyword, introduced in Lean 4, solves this by declaring the theorem signature*without*adding it to the environment\. The statement is visible for type\-checking but cannot be used as a lemma, closing the sorry\-exploitation loophole\. Additionally,proof\_wantedprevents the use ofnative\_decideand other kernel\-bypassing tactics, since no proof term is ever constructed\. We recommend that all benchmark datasets useproof\_wantedinstead ofsorryfor unsolved problem statements\.

Turn off auto\-implicit\.Most benchmarks are created by auto\-formalizing natural language with LLMs\. When the LLM mistypes a variable name or forgets to define a type parameter, Lean’s auto\-implicit feature silently “fixes” it by adding implicit parameters\. Lean’s default autoImplicit automatically inserts hidden type parameters and universe levels for undeclared symbols, which is ergonomic for humans but risky for NL→\\rightarrowLean pipelines\. The file type\-checks, so nobody notices\. The error only surfaces later when one tries to prove it and finds it either trivial or impossible\. Addingset\_option autoImplicit falsemakes these errors fail at formalization time instead of hiding them\. This forces errors at formalization time until all intended domains and binders are declared explicitly\.

Avoid using Axioms\.In Lean, writingaxiom h :ϕ\\phi\(orconstant h :ϕ\\phi\) asserts a proof ofϕ\\phiexists; any solver can then “solve” the item by citing h, which collapses evaluation and obscures whether the statement is even satisfiable\. We should therefore adopt a no\-axioms rule for dataset files: problem statements are encoded as definitions of propositions, never as axioms\.

Dataset Maintenance and Pinning\.When datasets are released, the Lean/mathlib version they are intended for should also be made clear, so it serves as a reference when being solved by a model in more recent Lean versions\. Regardless of if the dataset is autoformalized or human written, there isn’t always a mathematical equivalent in Lean and it is an evolving language so some definitions and ease of translation will change over time\.

Capture all requirements, not just the main claim\.While human verification is the gold standard for identifying errors in formalization, it is costly and time\-consuming\. LLM\-as\-a\-judge can be used as a triage tool to identify whether a formalization captures all requirements in a given statement rather than only the main claim\.

## 6Related Work

Formal math benchmarks and repair efforts\.Standard formal mathematics benchmarks include*miniF2F*\(Zhenget al\.,[2022](https://arxiv.org/html/2606.29493#bib.bib22)\),*ProofNet*\(Azerbayevet al\.,[2023](https://arxiv.org/html/2606.29493#bib.bib23)\),*FormalMath*\(Yuet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib24)\),*CombiBench*\(Liuet al\.,[2025a](https://arxiv.org/html/2606.29493#bib.bib26)\), and*ProverBench*\(Renet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib27)\)\. The closest repair\-oriented work is miniF2F\-v2\(Ospanovet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib45)\), which performs a detailed human audit of miniF2F, documents discrepancies between formal and informal statements, and releases repaired statements and proofs\. Our work is complementary: rather than presenting a fully repaired single benchmark, we audit a broader benchmark suite and focus on a taxonomy, scalable static checks, and release standards that help direct expert effort\.

Recent work on the Erdős problems database has highlighted both the promise and perils of AI\-assisted formalization at scale\(Alexeev,[2025](https://arxiv.org/html/2606.29493#bib.bib10)\)\. Alexeev developed an automated pipeline combining ChatGPT for proof explanation with Harmonic’s Aristotle system\(Achimet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib11)\)for autoformalization, successfully formalizing solutions to approximately ten problems with minimal human intervention\. Notably, Aristotle autonomously resolved Problem 124 by exploiting a weaker formulation than Erdős intended, a misformalization that went undetected until the AI found a trivial proof\. This experience underscores our findings: the same AI systems that accelerate formalization can also serve as effective detectors of specification errors, discovering missing hypotheses \(Problem 56\), incorrect variable constraints \(Problem 480 wherem≠\\neq0was written instead ofn≠\\neq0\), and vacuous hypotheses\.

##### Autoformalization and semantic\-fidelity evaluation\.

The task of translating informal mathematical statements into formal specifications has been studied extensively\(Wuet al\.,[2022](https://arxiv.org/html/2606.29493#bib.bib7); Jianget al\.,[2023](https://arxiv.org/html/2606.29493#bib.bib8)\)\. Recent work demonstrates that LLMs can produce syntactically correct Lean code at scale, though semantic fidelity remains challenging\(Poirouxet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib44); Liuet al\.,[2025b](https://arxiv.org/html/2606.29493#bib.bib42); Luet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib43)\)\.Liuet al\.\([2025c](https://arxiv.org/html/2606.29493#bib.bib41)\)scale theorem\-statement generation through lifting, augmentation, and synthesis;Liuet al\.\([2025b](https://arxiv.org/html/2606.29493#bib.bib42)\)propose a formal\-grounded equivalence metric and dependency retrieval for statement autoformalization;Luet al\.\([2025](https://arxiv.org/html/2606.29493#bib.bib43)\)evaluate alignment between informal and formal statements; andCabralet al\.\([2026](https://arxiv.org/html/2606.29493#bib.bib40)\)focus on preserving proof\-step structure via dependency graphs\. These works improve generation or evaluation of formalizations\. Our focus is orthogonal: we study benchmark defects and evaluation loopholes after statements enter the theorem\-proving evaluation pipeline\.

##### Specification errors in formal verification\.

The software verification community has long recognized that formal proofs guarantee correctness only relative to their specifications, and specification errors can be as dangerous as implementation bugs\(Woodcocket al\.,[2009](https://arxiv.org/html/2606.29493#bib.bib4)\)\. Studies of industrial verification efforts report that specification defects account for a substantial fraction of issues discovered during proof attempts\(Kleinet al\.,[2014](https://arxiv.org/html/2606.29493#bib.bib5)\)\. The seL4 microkernel verification, for instance, required extensive iteration to align formal specifications with intended behavior\(Kleinet al\.,[2009](https://arxiv.org/html/2606.29493#bib.bib6)\)\. Our work applies these lessons to the ML benchmarking setting, where the pressure to scale dataset creation amplifies specification risk\.

##### Counterexample generation\.

Automated counterexample finding has proven effective for detecting specification errors in proof assistants\. Isabelle’s Nitpick tool encodes higher\-order logic into first\-order relational logic and invokes SAT solvers to find finite countermodels\(Blanchette and Nipkow,[2010](https://arxiv.org/html/2606.29493#bib.bib1)\), while Quickcheck provides randomized testing\(Bulwahn,[2012](https://arxiv.org/html/2606.29493#bib.bib2)\)\. Adapting these techniques to dependent type theory remains challenging due to the richer type structure; recent progress includes Chako, which integrates Lean with the Nunchaku model finder\(Reynoldset al\.,[2016](https://arxiv.org/html/2606.29493#bib.bib3)\)\. Our vacuity and counterexample checkers draw on this tradition, though many benchmark defects still require semantic understanding beyond what current model finders can provide\.

## 7Limitations

We do not claim a complete human\-verified enumeration of all defects across all items in all datasets and their forks\. Some issues require mathematical insight \(e\.g\., whether a question is false or vacuous\) or Lean expertise \(e\.g\., translating mathematics into Lean with the correct encoding\)\. Our goal is to \(i\) demonstrate that defects are common enough to matter, \(ii\) propose checks and standards that prevent high\-impact failures, and \(iii\) make future benchmark development easier by releasing checkers and prompts\.

Our implementation is Lean\-specific, but the taxonomy is not\. Fidelity failures arise whenever natural\-language mathematics is translated into a formal language; evaluation loopholes arise whenever a solver is rewarded for passing an automated checker; and maintenance decay arises whenever libraries, proof assistants, or benchmark forks evolve\. Other proof assistants would require different static checks, for example different arithmetic totalization rules or axiom policies, but the audit structure transfers\.

## 8Conclusion & Future Work

Lean proof checking removes many sources of error in theorem proving evaluation, but it does not guarantee benchmark validity\. Specification fidelity is a known challenge across formal methods and ML evaluation, yet systematic audits of Lean theorem\-proving benchmarks have been lacking: a gap our taxonomy, checkers, and case studies aim to fill\.

Future work involves extending this to more benchmarks, generating better high\-quality synthetic data and filtering existing lean datasets, and developing an effective theorem proving harness\.

## Software and Data

Our static checkers \(implemented as Lean 4 metaprograms\), the evaluation harness, the semantic\-audit prompts, and snapshots of the audited benchmark variants are available at[https://github\.com/Shashi456/atp\-checkers](https://github.com/Shashi456/atp-checkers)\.

## Acknowledgements

We gratefully acknowledge support from Renaissance Philanthropy’s AI for Math Fund through the MathBench: Towards Evaluating Natural Language Proofs project\. We thank the AI for Math Fund team for supporting open research infrastructure at the intersection of artificial intelligence and mathematics\. The views expressed in this paper are those of the authors and do not necessarily reflect the views of the funders\.

## Impact Statement

This paper presents work aimed at advancing the field of formal mathematics benchmarking\. By identifying systematic issues in current benchmarks, we aim to improve the reliability of evaluations in automated theorem proving, leading to a more accurate assessment of progress in the field\. Our checkers and taxonomy can help benchmark creators catch defects before release, reducing the risk that published results reflect evaluation artifacts rather than genuine capability\. The release of our static checkers and LLM prompts may also improve the quality of training data for formal reasoning systems\. More broadly, documenting failure modes in formal verification pipelines enhances the trustworthiness of formally verified software, with implications for safety\-critical systems\. We also release these tools, hoping that they will be helpful in improving the data quality of pre\-training and post\-training\. As automated theorem provers are increasingly used to verify mathematical claims and software correctness, the integrity of their evaluation infrastructure becomes a matter of broader scientific trust\. We hope this work contributes to a culture of rigorous benchmark stewardship in the formal methods community\.

## References

- T\. Achim, A\. Best, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leister, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg, M\. Michelsen, R\. Patterson, E\. Rodriguez, L\. Scharff, V\. Shanker, V\. Sicca, H\. Sowrirajan, A\. Swope, M\. Tamas, V\. Tenev, J\. Thomm, H\. Williams, and L\. Wu \(2025\)Aristotle: IMO\-level automated theorem proving\.arXiv preprint arXiv:2510\.01346\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.p2.2)\.
- B\. Alexeev \(2025\)Formalization of Erdős problems\.Note:Xena \(blog\)Guest postExternal Links:[Link](https://xenaproject.wordpress.com/2025/12/05/formalization-of-erdos-problems/)Cited by:[§6](https://arxiv.org/html/2606.29493#S6.p2.2)\.
- 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\.12433Cited by:[item 2](https://arxiv.org/html/2606.29493#A1.I1.i2.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.p1.1)\.
- J\. C\. Blanchette and T\. Nipkow \(2010\)Nitpick: a counterexample generator for higher\-order logic based on a relational model finder\.InInternational Conference on Interactive Theorem Proving,pp\. 131–146\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px3.p1.1)\.
- L\. Bulwahn \(2012\)Smart testing of functional programs in Isabelle\.InInternational Conference on Logic for Programming, Artificial Intelligence, and Reasoning,pp\. 153–167\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px3.p1.1)\.
- R\. M\. Cabral, T\. M\. Do, Y\. Xuejun, W\. M\. Tai, Z\. Feng, and S\. Xin \(2026\)ProofFlow: a dependency graph approach to faithful proof autoformalization\.InInternational Conference on Learning Representations \(ICLR\),External Links:[Link](https://openreview.net/forum?id=s9t2FJVsBH)Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- L\. M\. de Moura, S\. Kong, J\. Avigad, F\. van Doorn, and J\. von Raumer \(2015\)The lean theorem prover \(system description\)\.InCADE,External Links:[Link](https://api.semanticscholar.org/CorpusID:232990)Cited by:[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px1.p1.1)\.
- F\. Dupuis, R\. Y\. Lewis, and H\. Macbeth \(2024\)Formalized functional analysis with semilinear maps\.Journal of Automated Reasoning68\(2\),pp\. 10\.Cited by:[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px1.p2.5)\.
- \[9\]harmonic CommunityHarmonic minif2f performance\.Note:[https://harmonic\.fun/news\#blog\-post\-2](https://harmonic.fun/news#blog-post-2)External Links:[Link](https://harmonic.fun/news#blog-post-2)Cited by:[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px2.p1.1)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample \(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.InInternational Conference on Learning Representations,Cited by:[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px2.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- G\. Klein, J\. Andronick, K\. Elphinstone, T\. Murray, T\. Sewell, R\. Kolanski, and G\. Heiser \(2014\)Comprehensive formal verification of an OS microkernel\.ACM Transactions on Computer Systems32\(1\),pp\. 1–70\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px2.p1.1)\.
- G\. Klein, K\. Elphinstone, G\. Heiser, J\. Andronick, D\. Cock, P\. Derrin, D\. Elkaduwe, K\. Engelhardt, R\. Kolanski, M\. Norrish,et al\.\(2009\)seL4: formal verification of an OS kernel\.InProceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles,pp\. 207–220\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px2.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 \(2026\)Goedel\-prover\-v2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=j4C0nALrgK)Cited by:[§1](https://arxiv.org/html/2606.29493#S1.p1.1)\.
- J\. Liu, X\. Lin, J\. Bayer, Y\. Dillies, W\. Jiang, X\. Liang, R\. Soletskyi, H\. Wang, Y\. Xie, B\. Xiong, Z\. Yang, J\. Zhang, L\. Zhi, J\. Li, and Z\. Liu \(2025a\)CombiBench: benchmarking llm capability for combinatorial mathematics\.External Links:2505\.03171,[Link](https://arxiv.org/abs/2505.03171)Cited by:[item 4](https://arxiv.org/html/2606.29493#A1.I1.i4.p1.1),[Appendix E](https://arxiv.org/html/2606.29493#A5.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.p1.1)\.
- Q\. Liu, X\. Zheng, X\. Lu, Q\. Cao, and J\. Yan \(2025b\)Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval\-based approach\.InInternational Conference on Learning Representations \(ICLR\),External Links:[Link](https://openreview.net/forum?id=hUb2At2DsQ)Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- X\. Liu, K\. Bao, J\. Zhang, Y\. Liu, Y\. Chen, Y\. Liu, Y\. Jiao, and T\. Luo \(2025c\)ATLAS: autoformalizing theorems through lifting, augmentation, and synthesis of data\.InAdvances in Neural Information Processing Systems \(NeurIPS\),External Links:[Link](https://arxiv.org/abs/2502.05567)Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- J\. Lu, Y\. Wan, Y\. Huang, J\. Xiong, Z\. Liu, and Z\. Guo \(2025\)FormalAlign: automated alignment evaluation for autoformalization\.InInternational Conference on Learning Representations \(ICLR\),External Links:[Link](https://openreview.net/forum?id=B5RrIFMqbe)Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- A\. Ospanov, F\. Farnia, and R\. Yousefzadeh \(2025\)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:[§A\.2](https://arxiv.org/html/2606.29493#A1.SS2.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.p1.1)\.
- A\. Paulino, D\. Testa, E\. Ayers, H\. Böving, J\. Limperg, S\. Gadgil, and S\. Bhat \(2024\)Metaprogramming in Lean 4\.External Links:[Link](https://github.com/arthurpaulino/lean4-metaprogramming-book)Cited by:[Appendix F](https://arxiv.org/html/2606.29493#A6.p1.1),[§4\.1](https://arxiv.org/html/2606.29493#S4.SS1.p1.1)\.
- A\. Poiroux, G\. Weiss, V\. Kunčak, and A\. Bosselut \(2025\)Reliable evaluation and benchmarks for statement autoformalization\.External Links:2406\.07222,[Link](https://arxiv.org/abs/2406.07222)Cited by:[§4\.3](https://arxiv.org/html/2606.29493#S4.SS3.p2.1),[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.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:[item 5](https://arxiv.org/html/2606.29493#A1.I1.i5.p1.1),[§1](https://arxiv.org/html/2606.29493#S1.p1.1),[§3\.2](https://arxiv.org/html/2606.29493#S3.SS2.SSS0.Px1.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.p1.1)\.
- A\. Reynolds, J\. C\. Blanchette, S\. Cruanes, and C\. Tinelli \(2016\)Model finding for recursive functions in SMT\.InInternational Joint Conference on Automated Reasoning,pp\. 133–151\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px3.p1.1)\.
- H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. D\. Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu, J\. Lu, H\. de Saxcé, B\. Bailey, C\. Song, C\. Xiao, D\. Zhang, E\. Zhang, F\. Pu, H\. Zhu, J\. Liu, J\. Bayer, J\. Michel, L\. Yu, L\. Dreyfus\-Schmidt, L\. Tunstall, L\. Pagani, M\. Machado, P\. Bourigault, R\. Wang, S\. Polu, T\. Barroyer, W\. Li, Y\. Niu, Y\. Fleureau, Y\. Hu, Z\. Yu, Z\. Wang, Z\. Yang, Z\. Liu, and J\. Li \(2025\)Kimina\-prover preview: towards large formal reasoning models with reinforcement learning\.External Links:2504\.11354,[Link](https://arxiv.org/abs/2504.11354)Cited by:[§1](https://arxiv.org/html/2606.29493#S1.p1.1),[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px2.p1.1)\.
- J\. Woodcock, P\. G\. Larsen, J\. Bicarregui, and J\. Fitzgerald \(2009\)Formal methods: practice and experience\.ACM Computing Surveys41\(4\),pp\. 1–36\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px2.p1.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022\)Autoformalization with large language models\.InAdvances in Neural Information Processing Systems,Vol\.35,pp\. 32353–32368\.Cited by:[§6](https://arxiv.org/html/2606.29493#S6.SS0.SSS0.Px1.p1.1)\.
- Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Y\. Zheng, H\. Xin, W\. Huang, Y\. Wen, and W\. Liu \(2025\)FormalMATH: benchmarking formal mathematical reasoning of large language models\.arXiv preprint arXiv:2505\.02735\.Cited by:[item 3](https://arxiv.org/html/2606.29493#A1.I1.i3.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.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,External Links:[Link](https://openreview.net/forum?id=9ZPegFuFTFv)Cited by:[item 1](https://arxiv.org/html/2606.29493#A1.I1.i1.p1.1),[§3\.3](https://arxiv.org/html/2606.29493#S3.SS3.SSS0.Px2.p1.1),[§6](https://arxiv.org/html/2606.29493#S6.p1.1)\.

## Appendix ADataset Details

Our goal is to demonstrate that defects are systematic, not anecdotal, and to identify checks that catch them early\.

### A\.1Popular Formal Math Datasets

We focus on widely used Lean datasets that collectively represent the standard evaluation suite for neural theorem provers:

1. 1\.miniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2606.29493#bib.bib22)\): 488 Olympiad\-level problems \(244 validation, 244 test\), originally released in Lean 3\.
2. 2\.ProofNet\(Azerbayevet al\.,[2023](https://arxiv.org/html/2606.29493#bib.bib23)\): 371 undergraduate\-level problems from textbooks \(analysis, algebra, topology\), released in Lean 3 with paired natural\-language statements and proofs\.
3. 3\.FormalMath\(Yuet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib24)\): 5,560 Lean 4 problems spanning from Olympiad challenges to undergraduate\-level theorems across algebra, applied mathematics, calculus, number theory, and discrete mathematics\. They also release FormalMath Lite, a carefully selected subset of 425 problems \(comprising 359 high school\-level and 66 undergraduate\-level problems\)\.
4. 4\.CombiBench\(Liuet al\.,[2025a](https://arxiv.org/html/2606.29493#bib.bib26)\): A benchmark comprising 100 combinatorial problems, each formalized in Lean 4 and paired with its corresponding informal statement\.
5. 5\.ProverBench\(Renet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib27)\): A benchmark dataset comprising 325 problems\. 15 are formalized from AIME 24 and 25\. The remaining 310 problems are drawn from curated textbook examples and educational tutorials\.

### A\.2Provenance of Audited Variants

Because ports, forks, and corrected re\-releases of these benchmarks proliferate \([Section3](https://arxiv.org/html/2606.29493#S3)\), and because papers rarely record which one they evaluated, we list the exact upstream source of every variant audited in[Table4](https://arxiv.org/html/2606.29493#S4.T4)\. The slugs in[Table8](https://arxiv.org/html/2606.29493#A1.T8)match theVariantcolumn of that table\. A few details warrant a note\. The miniF2Fv2candv2sentries are the “complete” and “statement” splits of the re\-verified miniF2F\-v2 release\(Ospanovet al\.,[2025](https://arxiv.org/html/2606.29493#bib.bib45)\)\. Thejustincasherandharmonicrows are the*same*corrected formalizations \(Harmonic’s re\-release\) packaged under different train/validation/test partitions; because the static checkers range over the entire file, their counts in[Table4](https://arxiv.org/html/2606.29493#S4.T4)coincide, and we list both because each is distributed and evaluated as a separate artifact\. Theyangky11andyangky11\-earlyrows are two commits of Kaiyu Yang’sminiF2F\-lean4repository: the currentmain\(commit6306b5f\) and an earlier commit \(7a2d40b, dated 2023\-11\-17\) that predates its later statement fixes\.

Table 8:Provenance of the1313audited variants in[Table4](https://arxiv.org/html/2606.29493#S4.T4)\.hfdenotes a Hugging Face release; where a variant mirrors a canonical repository, both are given\.BenchmarkVariantUpstream sourceFormalMATHall[https://huggingface\.co/datasets/SphereLab/FormalMATH\-All](https://huggingface.co/datasets/SphereLab/FormalMATH-All)FormalMATHlite[https://huggingface\.co/datasets/SphereLab/FormalMATH\-Lite](https://huggingface.co/datasets/SphereLab/FormalMATH-Lite)project:[https://github\.com/Sphere\-AI\-Lab/FormalMATH\-Bench](https://github.com/Sphere-AI-Lab/FormalMATH-Bench)ProverBenchdeepseek[https://huggingface\.co/datasets/deepseek\-ai/DeepSeek\-ProverBench](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench)ProofNetdeepseek[https://github\.com/deepseek\-ai/DeepSeek\-Prover\-V1\.5/blob/main/datasets/proofnet\.jsonl](https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/blob/main/datasets/proofnet.jsonl)ProofNetsharp\(\#\)[https://huggingface\.co/datasets/PAug/ProofNetSharp](https://huggingface.co/datasets/PAug/ProofNetSharp)miniF2Fv2c,v2s[https://github\.com/roozbeh\-yz/miniF2F\_v2](https://github.com/roozbeh-yz/miniF2F_v2)\(complete / statement splits\)miniF2Fyangky11[https://github\.com/yangky11/miniF2F\-lean4](https://github.com/yangky11/miniF2F-lean4), commit6306b5fminiF2Fyangky11\-early[https://github\.com/yangky11/miniF2F\-lean4](https://github.com/yangky11/miniF2F-lean4), commit7a2d40b\(2023\-11\-17\)miniF2Fjustincasher[https://github\.com/justincasher/miniF2F](https://github.com/justincasher/miniF2F)\(Harmonic’s formalizations, original miniF2F splits\)miniF2Fharmonic[https://github\.com/harmonic\-ai/datasets/tree/main/minif2f](https://github.com/harmonic-ai/datasets/tree/main/minif2f)\(same formalizations, Harmonic’s own splits\)miniF2Fai\-mo[https://huggingface\.co/datasets/AI\-MO/minif2f\_test](https://huggingface.co/datasets/AI-MO/minif2f_test)CombiBenchhf[https://huggingface\.co/datasets/AI\-MO/CombiBench](https://huggingface.co/datasets/AI-MO/CombiBench)canonical:[https://github\.com/MoonshotAI/CombiBench](https://github.com/MoonshotAI/CombiBench)

## Appendix BIssues in Formal Mathematics Datasets

This appendix has examples of various formalization issues found across major formal mathematics benchmarks\. We present side\-by\-side comparisons of problematic formalizations, and describe the error and either point out which version is correct or provide the correction\. This section is meant to familiarize the reader with the kinds of pitfalls we observe in datasets\. This is not a complete list of all errors in datasets like miniF2F, ProofNet, FormalMath, ProverBench which would span 100s of problems if not 1000s\.

### B\.1Issue 1: Incomplete Formalization

Many problems in formal benchmarks only formalize part of the original problem, often missing crucial constraints or conditions\.

#### B\.1\.1IMO 1983 Problem 6 \- miniF2F

In this problem, the solution must first prove the inequality and then determine when equality occurs\.

Problem StatementProblem:Letaa,bbandccbe the lengths of the sides of a triangle\. Prove thata2​b​\(a−b\)\+b2​c​\(b−c\)\+c2​a​\(c−a\)≥0\.a^\{2\}b\(a\-b\)\+b^\{2\}c\(b\-c\)\+c^\{2\}a\(c\-a\)\\geq 0\.Determine when equality occurs\.

DSP/OpenAI/Numina Version[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9fMTk4M19wNgogIChhIGIgYyA6IOKEnSkKICAoaOKCgCA6IDAgPCBhIOKIpyAwIDwgYiDiiKcgMCA8IGMpCiAgKGjigoEgOiBjIDwgYSArIGIpCiAgKGjigoIgOiBiIDwgYSArIGMpCiAgKGjigoMgOiBhIDwgYiArIGMpIDoKICAwIOKJpCBhXjIgKiBiICogKGEgLSBiKSArCiAgICAgIGJeMiAqIGMgKiAoYiAtIGMpICsKICAgICAgY14yICogYSAqIChjIC0gYSkgOj0KYmVnaW4KICBzb3JyeQplbmQ=)1theorem𝒫\\mathscr\{P\}imo\_1983\_p62𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}c\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h3𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}:7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}a^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}\+8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}b^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(b𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}\+9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}c^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(c𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}a\)𝒫\\mathscr\{P\}:=10begin11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry12end

Harmonic Version \(Correct\)[⬇](data:text/plain;base64,dGhlb3JlbSBmb3JtYWxfMTY0NwogIChhIGIgYyBkIDog4oSdKQogICho4oKAIDogMCA8IGEg4oinIDAgPCBiIOKIpyAwIDwgYykKICAoaOKCgSA6IGMgPCBhICsgYikKICAoaOKCgiA6IGIgPCBhICsgYykKICAoaOKCgyA6IGEgPCBiICsgYykKICAoaOKChCA6IGQgPSBhXjIgKiBiICogKGEgLSBiKSArCiAgICAgICAgICAgYl4yICogYyAqIChiIC0gYykgKwogICAgICAgICAgIGNeMiAqIGEgKiAoYyAtIGEpKSA6CiAgMCDiiaQgZCDiiKcgKGQgPSAwIOKGlCAoYSA9IGIg4oinIGIgPSBjKSkgOj0gYnkKICBzb3JyeQ==)1theorem𝒫\\mathscr\{P\}formal\_16472𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}d𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}c\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h3𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}c\)7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h4𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}d𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}a^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}\+8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}b^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}c𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(b𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}c\)𝒫\\mathscr\{P\}\+9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}c^2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}\(c𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}a\)\)𝒫\\mathscr\{P\}:10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}d𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}\(d𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}↔\\leftrightarrow𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}c\)\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

#### B\.1\.2IMO 1981 Problem 6 \- miniF2F

The problem asks to “Determinef​\(4,1981\)f\(4,1981\)” – a specific computational problem requiring finding an actual value\. While the formalization asks for a recurrence relationf​\(4,y\+1\)=2f​\(4,y\)\+3−3f\(4,y\+1\)=2^\{f\(4,y\)\+3\}\-3\. While it might be the case that the recurrence relation might be used to solve the computational problem, this is not an exact formalization\. Proving the recurrence is necessary but not sufficient for computing the numerical value\.

Problem StatementProblem:The functionf​\(x,y\)f\(x,y\)satisfies: \(1\)f​\(0,y\)=y\+1f\(0,y\)=y\+1, \(2\)f​\(x\+1,0\)=f​\(x,1\)f\(x\+1,0\)=f\(x,1\), \(3\)f​\(x\+1,y\+1\)=f​\(x,f​\(x\+1,y\)\)f\(x\+1,y\+1\)=f\(x,f\(x\+1,y\)\), for all non\-negative integersx,yx,y\. Determinef​\(4,1981\)f\(4,1981\)\.

DSP version[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9fMTk4MV9wNgogIChmIDog4oSVIOKGkiDihJUg4oaSIOKElSkKICAoaOKCgCA6IOKIgCB5LCBmIDAgeSA9IHkgKyAxKQogICho4oKBIDog4oiAIHgsIGYgKHggKyAxKSAwID0gZiB4IDEpCiAgKGjigoIgOiDiiIAgeCB5LCBmICh4ICsgMSkgKHkgKyAxKSA9CiAgICAgICBmIHggKGYgKHggKyAxKSB5KSkgOgogIOKIgCB5LCBmIDQgKHkgKyAxKSA9CiAgMl4oZiA0IHkgKyAzKSAtIDMgOj0KYmVnaW4KICBzb3JyeQplbmQ=)1theorem𝒫\\mathscr\{P\}imo\_1981\_p62𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(f𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}x,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}1\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}\(y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}=6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\(f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}y\)\)𝒫\\mathscr\{P\}:7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}\(y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}=8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}2^\(f𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}3\)𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}:=9begin10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry11end

Harmonic version[⬇](data:text/plain;base64,dGhlb3JlbSBmb3JtYWxfMTUxNAogIChmIDog4oSVIOKGkiDihJUg4oaSIOKElSkKICAoaOKCgCA6IOKIgCB5LCBmIDAgeSA9IHkgKyAxKQogICho4oKBIDog4oiAIHgsIGYgKHggKyAxKSAwID0gZiB4IDEpCiAgKGjigoIgOiDiiIAgeCB5LCBmICh4ICsgMSkgKHkgKyAxKSA9CiAgICAgICBmIHggKGYgKHggKyAxKSB5KSkgOgogIOKIgCB5LCBmIDQgKHkgKyAxKSA9CiAgMl4oZiA0IHkgKyAzKSAtIDMgOj0gYnkKICBzb3JyeQ==)1theorem𝒫\\mathscr\{P\}formal\_15142𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(f𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}x,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}1\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}\(y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}=6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\(f𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}y\)\)𝒫\\mathscr\{P\}:7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}y,𝒫\\mathscr\{P\}f𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}\(y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}=8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}2^\(f𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}3\)𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

#### B\.1\.3Axler Exercise 3\.8 \- ProofNet

The formalization is missing the properties of V where it should be finite dimensional\. The existence of complements/kernel intersections depends on finite\-dimensionality; otherwiseU∩ker⁡T=\{0\}U\\cap\\ker T=\\\{0\\\}withrange​T=T​\(U\)\\text\{range \}T=T\(U\)need not hold\.

Problem StatementProblem:Suppose thatVVis finite dimensional and thatT∈ℒ​\(V,W\)T\\in\\mathcal\{L\}\(V,W\)\. Prove that there exists a subspaceUUofVVsuch thatU∩null​T=\{0\}U\\cap\\text\{null \}T=\\\{0\\\}and rangeT=\{T​u:u∈U\}T=\\\{Tu:u\\in U\\\}\.

ProofNet \- Axler Exercise 3\.8 \(Missing finite dimension hypothesis\)[⬇](data:text/plain;base64,dGhlb3JlbSBleGVyY2lzZV8zXzgge0YgViBXIDogVHlwZSp9IFthZGRfY29tbV9ncm91cCBWXQogIFthZGRfY29tbV9ncm91cCBXXSBbZmllbGQgRl0gW21vZHVsZSBGIFZdIFttb2R1bGUgRiBXXQogIChMIDogViDihpJbRl0gVykgOgogIOKIgyBVIDogc3VibW9kdWxlIEYgViwgVSDiipMgTC5rZXIgPSDiiqUg4oinCiAgbGluZWFyX21hcC5yYW5nZSBMID0gcmFuZ2UgKGRvbV9yZXN0cmljdCBMIFUpOj0=)1theorem𝒫\\mathscr\{P\}exercise\_3\_8𝒫\\mathscr\{P\}\{F𝒫\\mathscr\{P\}V𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Type\*\}𝒫\\mathscr\{P\}\[add\_comm\_group𝒫\\mathscr\{P\}V\]2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\[add\_comm\_group𝒫\\mathscr\{P\}W\]𝒫\\mathscr\{P\}\[field𝒫\\mathscr\{P\}F\]𝒫\\mathscr\{P\}\[module𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}V\]𝒫\\mathscr\{P\}\[module𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}W\]3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(L𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}V𝒫\\mathscr\{P\}→\\rightarrow\[F\]𝒫\\mathscr\{P\}W\)𝒫\\mathscr\{P\}:4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}U𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}submodule𝒫\\mathscr\{P\}F𝒫\\mathscr\{P\}V,𝒫\\mathscr\{P\}U𝒫\\mathscr\{P\}⊓\\sqcap𝒫\\mathscr\{P\}L\.ker𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}⊥\\bot𝒫\\mathscr\{P\}∧\\land5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}linear\_map\.range𝒫\\mathscr\{P\}L𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}range𝒫\\mathscr\{P\}\(dom\_restrict𝒫\\mathscr\{P\}L𝒫\\mathscr\{P\}U\):=

### B\.2Issue: Missing Specification

#### B\.2\.1IMO 1962 Problem 2 \- miniF2F

The DSP/numina version doesn’t specify that3−x−x\+1\>0\\sqrt\{3\-x\}\-\\sqrt\{x\+1\}\>0, and while it might be perhaps immaterial while solving the problem, it is a case of missing specification and leaving nothing to ambiguity\.

Problem StatementProblem:Show that if the real numberxxsatisfies the inequality3−x−x\+1<12\\sqrt\{\\sqrt\{3\-x\}\-\\sqrt\{x\+1\}\}<\\frac\{1\}\{2\}, then−1≤x<1−12732\-1\\leq x<1\-\\frac\{\\sqrt\{127\}\}\{32\}\.

DSP/Numina version[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9fMTk2Ml9wMgogICh4IDog4oSdKQogICho4oKTIDogMCDiiaQgMyAtIHgpCiAgKGjigoEgOiAwIOKJpCB4ICsgMSkKICAoaOKCgiA6IDEgLyAyIDwgcmVhbC5zcXJ0ICgzIC0geCkgLQogICAgICAgcmVhbC5zcXJ0ICh4ICsgMSkpIDoKICAtMSDiiaQgeCDiiKcgeCA8IDEgLQogIHJlYWwuc3FydCAzMSAvIDggOj0KYmVnaW4KICBzb3JyeQplbmQ=)1theorem𝒫\\mathscr\{P\}imo\_1962\_p22𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hx𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}x\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}/𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}real\.sqrt𝒫\\mathscr\{P\}\(3𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}x\)𝒫\\mathscr\{P\}\-6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}real\.sqrt𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)\)𝒫\\mathscr\{P\}:7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\-1𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}\-8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}real\.sqrt𝒫\\mathscr\{P\}31𝒫\\mathscr\{P\}/𝒫\\mathscr\{P\}8𝒫\\mathscr\{P\}:=9begin10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry11end

Harmonic version[⬇](data:text/plain;base64,dGhlb3JlbSBmb3JtYWxfNDUxOAogICh4IDog4oSdKQogICho4oKTIDogeCDiiaQgMykKICAoaOKCgSA6IC0xIOKJpCB4KQogICho4oKCIDogMCDiiaQgUmVhbC5zcXJ0ICgzIC0geCkgLQogICAgICAgUmVhbC5zcXJ0ICh4ICsgMSkpCiAgKGjigoMgOiBSZWFsLnNxcnQgKFJlYWwuc3FydCAoMyAtIHgpIC0KICAgICAgIFJlYWwuc3FydCAoeCArIDEpKSA+IDEgLyAyKSA6CiAgLTEg4omkIHgg4oinIHggPCAxIC0KICBSZWFsLnNxcnQgMTI3IC8gMzIgOj0gYnkKICBzb3JyeQ==)1theorem𝒫\\mathscr\{P\}formal\_45182𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hx𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}3\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\-1𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}x\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}\(3𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}x\)𝒫\\mathscr\{P\}\-6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)\)7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h3𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}\(Real\.sqrt𝒫\\mathscr\{P\}\(3𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}x\)𝒫\\mathscr\{P\}\-8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)\)𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}/𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}:9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\-1𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}\-10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}127𝒫\\mathscr\{P\}/𝒫\\mathscr\{P\}32𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

#### B\.2\.2APMO 1991 Problem 2 \- CombiBench

In this problem originally, the points were not assumed to be distinct, so it was trivially false\. It was later fixed\.

Problem StatementProblem:Suppose there are 997 points given in a plane\. If every two points are joined by a line segment with its midpoint coloured in red, show that there are at least 1991 red points in the plane\.

Version 1[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCm5vbmNvbXB1dGFibGUgZGVmIHJlZF9wb2ludHMge2t9CiAgKHBvaW50cyA6IEZpbiBrIOKGkiDihJ0gw5cg4oSdKSA6CiAgRmluc2V0ICjihJ0gw5cg4oSdKSA6PQogICgoRmluc2V0LnVuaXYgKM6xIDo9IEZpbiBrIMOXIEZpbiBrKSkuaW1hZ2UKICAgIChmdW4geCA9PiBtaWRwb2ludCDihJ0gKHBvaW50cyB4LjEpCiAgICAgICAgICAgICAgICAgICAgICAgICAocG9pbnRzIHguMikpKQoKdGhlb3JlbSBhcG1vXzE5OTFfcDIKICAocG9pbnRzIDogRmluIDk5NyDihpIg4oSdIMOXIOKEnSkgOgogIChyZWRfcG9pbnRzIHBvaW50cykuY2FyZCDiiaUgMTk5MSA6PSBieQogIHNvcnJ5)1import𝒫\\mathscr\{P\}Mathlib23noncomputable𝒫\\mathscr\{P\}def𝒫\\mathscr\{P\}red\_points𝒫\\mathscr\{P\}\{k\}4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}:5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Finset𝒫\\mathscr\{P\}\(ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}:=6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(\(Finset\.univ𝒫\\mathscr\{P\}\(α\\alpha𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k\)\)\.image7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(fun𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=\>𝒫\\mathscr\{P\}midpoint𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}x\.1\)8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}x\.2\)\)\)910theorem𝒫\\mathscr\{P\}apmo\_1991\_p211𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}997𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}:12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(red\_points𝒫\\mathscr\{P\}points\)\.card𝒫\\mathscr\{P\}≥\\geq𝒫\\mathscr\{P\}1991𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by13𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

Fixed[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCm5vbmNvbXB1dGFibGUgZGVmIHJlZF9wb2ludHMge2t9CiAgKHBvaW50cyA6IEZpbiBrIOKGkiDihJ0gw5cg4oSdKSA6CiAgRmluc2V0ICjihJ0gw5cg4oSdKSA6PQooKChGaW5zZXQudW5pdiAozrEgOj0gRmluIGsgw5cgRmluIGspKSBcCiAgKEZpbnNldC51bml2KS5pbWFnZSAoZnVuIGkgPT4gKGksIGkpKSkuaW1hZ2UKICAgIChmdW4geCA9PiBtaWRwb2ludCDihJ0gKHBvaW50cyB4LjEpCiAgICAgICAgICAgICAgICAgICAgICAgICAocG9pbnRzIHguMikpKQoKdGhlb3JlbSBhcG1vXzE5OTFfcDIgKHBvaW50cyA6IEZpbiA5OTcg4oaSIOKEnSDDlyDihJ0pCiAgKGhwb2ludHMgOiBGdW5jdGlvbi5JbmplY3RpdmUgcG9pbnRzKSA6CiAgKHJlZF9wb2ludHMgcG9pbnRzKS5jYXJkIOKJpSAxOTkxIDo9IGJ5CiAgc29ycnk=)1import𝒫\\mathscr\{P\}Mathlib23noncomputable𝒫\\mathscr\{P\}def𝒫\\mathscr\{P\}red\_points𝒫\\mathscr\{P\}\{k\}4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}:5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}Finset𝒫\\mathscr\{P\}\(ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}:=6\(\(\(Finset\.univ𝒫\\mathscr\{P\}\(α\\alpha𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k\)\)𝒫\\mathscr\{P\}\\7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(Finset\.univ\)\.image𝒫\\mathscr\{P\}\(fun𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}=\>𝒫\\mathscr\{P\}\(i,𝒫\\mathscr\{P\}i\)\)\)\.image8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(fun𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=\>𝒫\\mathscr\{P\}midpoint𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}x\.1\)9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}x\.2\)\)\)1011theorem𝒫\\mathscr\{P\}apmo\_1991\_p2𝒫\\mathscr\{P\}\(points𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}997𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hpoints𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Function\.Injective𝒫\\mathscr\{P\}points\)𝒫\\mathscr\{P\}:13𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(red\_points𝒫\\mathscr\{P\}points\)\.card𝒫\\mathscr\{P\}≥\\geq𝒫\\mathscr\{P\}1991𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by14𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

### B\.3Issue: Incorrect Translation

Some formalizations fundamentally misrepresent the original problem, leading to different mathematical statements\.

#### B\.3\.1MATHD Algebra 15 \- miniF2F

In this case, Harmonic version doesn’t capture the general operation definition from the problem statement instead it directly introduces the substituted weaker version of the problem to solve\. DSP and OpenAI versions define a general operationsswhile Harmonic directly computes the specific case\.

Problem StatementProblem:Ifa∗b=ab\+baa\*b=a^\{b\}\+b^\{a\}, for all positive integer values ofaaandbb, show that2∗6=1002\*6=100

DSP Version[⬇](data:text/plain;base64,dGhlb3JlbSBtYXRoZF9hbGdlYnJhXzE1CiAgKHMgOiDihJUg4oaSIOKElSDihpIg4oSVKQogICho4oKAIDog4oiAIGEgYiwgMCA8IGEg4oinIDAgPCBiIOKGkgogICBzIGEgYiA9IGFeKGI64oSVKSArIGJeKGE64oSVKSkgOgogIHMgMiA2ID0gMTAwIDo9CmJlZ2luCiAgcncgaOKCgCwKICByZWZsLAogIG5vcm1fbnVtLAplbmQ=)1theorem𝒫\\mathscr\{P\}mathd\_algebra\_152𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(s𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}b,𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}→\\rightarrow4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}s𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}a^\(b:ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b^\(a:ℕ\\mathbb\{N\}\)\)𝒫\\mathscr\{P\}:5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}s𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}6𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}100𝒫\\mathscr\{P\}:=6begin7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}rw𝒫\\mathscr\{P\}h0,8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}refl,9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}norm\_num,10end

Harmonic Version[⬇](data:text/plain;base64,dGhlb3JlbSBmb3JtYWxfMjg5NSA6CiAgMiBeIDYgKyA2IF4gMiA9IDEwMCA6PSBieQogIHNvcnJ5)1theorem𝒫\\mathscr\{P\}formal\_2895𝒫\\mathscr\{P\}:2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}6𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}6𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}100𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

OpenAI Version[⬇](data:text/plain;base64,dGhlb3JlbSBtYXRoZF9hbGdlYnJhXzE1CiAgKHMgOiDihJUg4oaSIOKElSDihpIg4oSVKQogICho4oKAIDog4oiAIGEgYiwgMCA8IGEg4oinIDAgPCBiIOKGkgogICBzIGEgYiA9IGFeKGI64oSVKSArIGJeKGE64oSVKSkgOgogIHMgMiA2ID0gMTAwIDo9CmJlZ2luCiAgcncgaOKCgCwKICByZWZsLAogIG5vcm1fbnVtLAplbmQ=)1theorem𝒫\\mathscr\{P\}mathd\_algebra\_152𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(s𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}b,𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}→\\rightarrow4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}s𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}a^\(b:ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}b^\(a:ℕ\\mathbb\{N\}\)\)𝒫\\mathscr\{P\}:5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}s𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}6𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}100𝒫\\mathscr\{P\}:=6begin7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}rw𝒫\\mathscr\{P\}h0,8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}refl,9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}norm\_num,10end

#### B\.3\.2Number Theory Problem 2 \- ProverBench

In this, problem u is a free variable and the specification that u is a substitute fory−2​xy\-2xis missing\. Not only that, upon further look there might be an error in the problem, wherex\+u​3x\+u\\sqrt\{3\}does not solve the question, and the actual problem should haveu\+x​3u\+x\\sqrt\{3\}\.

Problem StatementProblem:For the equationx2\+y2−1=4​x​yx^\{2\}\+y^\{2\}\-1=4xyits general solution in the integers is given byx\+u​3=\(2\+3\)nx\+u\\sqrt\{3\}=\(2\+\\sqrt\{3\}\)^\{n\}, whereuuis the substitute fory−2​xy\-2x\.

ProverBench Formalization \(Incorrect\)[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCnRoZW9yZW0gZ2VuZXJhbF9zb2x1dGlvbl9xdWFkcmF0aWNfZXF1YXRpb24gKHggeSA6IOKEpCkgKHUgOiDihKQpIChuIDog4oSVKSA6CiAgeF4yICsgeV4yIC0gMSA9IDQgKiB4ICogeSDihpIgeCArIHUgKiBSZWFsLnNxcnQgMyA9ICgyICsgUmVhbC5zcXJ0IDMpXm4gOj0KICBzb3JyeQ==)1import𝒫\\mathscr\{P\}Mathlib23theorem𝒫\\mathscr\{P\}general\_solution\_quadratic\_equation𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}\)𝒫\\mathscr\{P\}\(u𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}\)𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}:4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}x^2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}y^2𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}y𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}u𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}\(2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}Real\.sqrt𝒫\\mathscr\{P\}3\)^n𝒫\\mathscr\{P\}:=5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

### B\.4Issue: Wrong Specification

#### B\.4\.1quantitative\_reasoning\_zh\_blue\_41 \- FormalMath Problem 5164

In this problem, truncated subtraction occurs due to natural numbers, and this is incorrect typecasting\.

Problem StatementProblem:GivenM=\{x∣x=a2\+1,a∈ℕ∗\}M=\\\{x\\mid x=a^\{2\}\+1,a\\in\\mathbb\{N\}^\{\*\}\\\},N=\{x∣x=b2−4​b\+5,b∈ℕ∗\}N=\\\{x\\mid x=b^\{2\}\-4b\+5,b\\in\\mathbb\{N\}^\{\*\}\\\}, then the relationship betweenMMandNNis Proof: The answer isM⊆NM\\subseteq N\. Froma2\+1=\(a\+2\)2−4​a\+5a^\{2\}\+1=\(a\+2\)^\{2\}\-4a\+5, we can see thatM⊆NM\\subseteq N\. However,1∈N1\\in Nand1∉M1\\notin M\.

FormalMath 5164[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKCm9wZW4gU2V0IFJlYWwKb3BlbiBzY29wZWQgQmlnT3BlcmF0b3JzCgp0aGVvcmVtIHF1YW50aXRhdGl2ZV9yZWFzb25pbmdfemhfYmx1ZV80MSA6CiAge3ggOiDihJUgfCDiiIMgYSA6IOKElSwgMCA8IGEg4oinIHggPSBhXjIgKyAxfSDiioIge3ggOiDihJUgfAogIOKIgyBiIDog4oSVLCAwIDwgYiDiiKcgeCA9IGJeMiAtIDQgKiBiICsgNX0gOj0gYnkKICBzb3JyeQ==)1import𝒫\\mathscr\{P\}Mathlib23open𝒫\\mathscr\{P\}Set𝒫\\mathscr\{P\}Real4open𝒫\\mathscr\{P\}scoped𝒫\\mathscr\{P\}BigOperators56theorem𝒫\\mathscr\{P\}quantitative\_reasoning\_zh\_blue\_41𝒫\\mathscr\{P\}:7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\{x𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}\|𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\},𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}a^2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\}𝒫\\mathscr\{P\}⊂\\subset𝒫\\mathscr\{P\}\{x𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}\|8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\},𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}b^2𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}4𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}5\}𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

#### B\.4\.2Problem 48 \- FormalMath

This does not avoid the case that n can take the value 0\.

Problem StatementProblem:If the sequence\{an\}\\\{a\_\{n\}\\\}satisfies that for anyn∈ℕ∗n\\in\\mathbb\{N\}^\{\*\},∑d\|nad=2n\\sum\_\{d\|n\}a\_\{d\}=2^\{n\}, prove thatn∣ann\\mid a\_\{n\}\.

FormalMath Formalization[⬇](data:text/plain;base64,dGhlb3JlbSBhbGdlYnJhXzU2NTUyIChhIDog4oSVIOKGkiDihJUpIChoYSA6IOKIgCBuLCDiiJEgZCBpbiBuLmRpdmlzb3JzLCBhIGQgPSAyIF4gbikgOgogIOKIgCBuLCBuIOKIoyBhIG4gOj0gYnkKICBzb3JyeQ==)1theorem𝒫\\mathscr\{P\}algebra\_56552𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\(ha𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}n,𝒫\\mathscr\{P\}∑\\sum𝒫\\mathscr\{P\}d𝒫\\mathscr\{P\}in𝒫\\mathscr\{P\}n\.divisors,𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}d𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}:2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}n,𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}∣\\mid𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

## Appendix CFault Taxonomy: Detailed Definitions

This appendix provides detailed definitions and examples for each error category in our taxonomy\.

### C\.1Specification Errors vs\. Formalization Errors

The distinction between specification and formalization errors is crucial for understanding benchmark defects\.

##### Specification errors

occur when the formalization is*incomplete*—it omits content that should be present\. The Lean statement is a proper subset of what the informal problem requires:

- •Missing hypotheses: The informal problem states conditions not encoded in Lean\. Example: “SupposeVVis finite\-dimensional” becomes a theorem about general vector spaces\.
- •Missing subgoals: Multi\-part problems have some parts dropped\. Example: “ProvePPand determine when equality holds” becomes a theorem proving onlyPP\.
- •Underspecified constraints: Implicit mathematical conventions are not made explicit\. Example: “for positive integers” uses\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)without\(hn𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}n\)\.

A specification error in isolation typically makes a problem*easier*\(fewer constraints, fewer subgoals to prove\)\.

##### Formalization errors

occur when the translation*misrepresents*the original—not by omission, but by encoding something different:

- •Incorrect translation: The mathematical content is mistranslated\. Example: “xxdividesyy” encoded asx/yx/y\(division\) instead ofx∣yx\\mid y\(divisibility\)\.
- •Encoding artifacts: The translation introduces structure not in the original\. Example: encoding an existential with a specific witness constrains solutions\.
- •Logic errors: Wrong quantifier scope, implication direction, or connectives\. Example:∀x,P​\(x\)→∃y,Q​\(y\)\\forall x,P\(x\)\\to\\exists y,Q\(y\)vs\.∃y,∀x,P​\(x\)→Q​\(y\)\\exists y,\\forall x,P\(x\)\\to Q\(y\)\.

A formalization error may make a problem easier, harder, or*impossible*to prove correctly\.

##### Remediation differs\.

- •Specification errors require*adding*content: insert missing hypotheses, add subgoals, make constraints explicit\.
- •Formalization errors require*correcting*content: fix mistranslations, remove artifacts, restructure logic\.

### C\.2Domain and Type Mismatches

A special class of formalization errors where the mathematical domain is incorrectly encoded:

##### Wrong number system\.

Usingℕ\\mathbb\{N\}whenℤ\\mathbb\{Z\}orℝ\\mathbb\{R\}is intended\. This is particularly dangerous because:

- •Nat subtraction truncates:5𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}7𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0
- •No negative numbers: statements about “all integers” become statements about naturals
- •Division semantics differ across types

##### Incorrect type structure\.

- •UsingListwhenSetorFinsetis needed \(ordering, duplicates\)
- •Encoding bijections as two functions instead ofEquiv
- •UsingTypewhenPropwould be more appropriate

##### Coercion hazards\.

- •Int\.toNattruncates negatives to 0
- •Coercingℕ\\mathbb\{N\}toℝ\\mathbb\{R\}loses decidability of equality
- •Implicit coercions can hide type mismatches

### C\.3Definition Mismatches

The formalization uses the wrong mathematical definition:

##### Outdated definitions\.

Using hand\-rolled definitions when mathlib provides standard ones\. Example: defining “perfect set” as “closed and every point is a cluster point” instead of usingPerfect\.

##### Subtly different concepts\.

- •IsClosedvs\.IsCompactvs\.Perfect
- •Continuousvs\.Differentiablevs\.ContDiff
- •Subgroupvs\.Submonoidvs\.Subsemigroup

##### Wrong level of generality\.

Stating a theorem about groups when it requires rings, or over\-specializing toℝ\\mathbb\{R\}when the result holds for any ordered field\.

### C\.4Quantifier and Indexing Mismatches

##### Quantifier scope errors\.

Whether a variable is bound at statement level or inside the formula:

- •∀ϵ\>0,∃δ\\forall\\epsilon\>0,\\exists\\delta\(correct for limits\)
- •∃δ,∀ϵ\>0\\exists\\delta,\\forall\\epsilon\>0\(wrong—δ\\deltacannot depend onϵ\\epsilon\)

##### Indexing conventions\.

Mathematical statements often use 1\-indexed sequences \(“a1,a2,…,ana\_\{1\},a\_\{2\},\\ldots,a\_\{n\}”\); Lean’sFin𝒫\\mathscr\{P\}nandListare 0\-indexed\. Off\-by\-one errors can make statements false or vacuously true\.

##### Unused binders\.

Quantified variables that don’t appear in the formula body:

theorem𝒫\\mathscr\{P\}problem𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}IsLeast𝒫\\mathscr\{P\}\{k𝒫\\mathscr\{P\}\|𝒫\\mathscr\{P\}\.\.\.\}𝒫\\mathscr\{P\}100𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}

Often indicates copy\-paste errors or incomplete translation\.

### C\.5Lean Encoding Hazards

These are syntactically identifiable patterns that can silently change semantics:

##### Natural number subtraction\.

Inℕ\\mathbb\{N\}, subtraction is truncated:a𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0whenb≥ab\\geq a\. This affects:

- •Difference expressions:n𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}1is 0 whenn𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0
- •Loop bounds: iterating fromn𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}ktonmay iterate 0 times
- •Inequalities:a𝒫\\mathscr\{P\}\-𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}cbehaves unexpectedly near zero

##### Division and modulo by zero\.

In mathlib fields and division rings:

- •a𝒫\\mathscr\{P\}/𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0\(not undefined\)
- •0\-1𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0
- •n𝒫\\mathscr\{P\}%𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}nfor natural numbers

Unguarded denominators can trivialize goals or make false statements provable\.

##### Totalized analytic functions\.

Mathlib totalizes partial functions with junk values:

- •Real\.sqrt𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0forx<0x<0
- •Real\.log𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0forx≤0x\\leq 0
- •Real\.arcsin𝒫\\mathscr\{P\}x𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}0for\|x\|\>1\|x\|\>1

### C\.6Evaluation Loopholes

##### Axiom injection\.

If the environment containsaxiom𝒫\\mathscr\{P\}h𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}P, any solver can provePPby citingh\. This collapses evaluation—we cannot tell if the model found a real proof\.

##### Theapply?bug\.

In Lean<<4\.20\.0,apply?could introduce a synthetic sorry without logging errors\. Combined with universe\-level mismatches, this caused Lean to report success while the theorem was never kernel\-verified\. See Appendix[D](https://arxiv.org/html/2606.29493#A4)for examples\.

##### Overly powerful automation\.

- •native\_decidecan brute\-force decidable goals
- •decideon incorrectly\-typed goals can succeed trivially
- •Unrestrictedsimpwith\[\*\]may exploit unintended lemmas

### C\.7Maintenance and Source Issues

##### Source validity problems\.

- •Defective NL statements \(typos, ambiguity, mathematical errors\)
- •False claims \(the theorem is actually not true\)
- •Ambiguous specifications admitting multiple interpretations

##### Version drift\.

- •Lean 3→\\to4 migration changes syntax and semantics
- •Mathlib API changes rename or restructure definitions
- •Tactic behavior changes between Lean versions

##### Fork proliferation\.

Multiple versions of datasets coexist with:

- •Inconsistent train/val/test splits
- •Undocumented corrections \(some forks fix bugs, others don’t\)
- •Unclear lineage \(which version is upstream?\)

Papers rarely specify which fork they used, making cross\-paper comparisons unreliable\.

## Appendix DTheapply?Frontend Bug: Example Exploits

The following proofs, generated by DeepSeek\-Prover\-V2\-7B on PutnamBench, trigger a frontend bug in Lean 4\.9\.0 whereapply?combined with a universe\-level error causes Lean to silently drop the theorem without kernel verification\. The bug occurs becauseapply?callsadmitGoalwithout logging errors, creating a synthetic sorry\. When elaboration encounters a universe parameter error, it stops beforeaddDeclis reached, so the expected “declaration uses sorry” warning is never emitted\.

Problem StatementPutnam 2005\-A4:LetHHbe ann×nn\\times nmatrix all of whose entries are±1\\pm 1and whose rows are mutually orthogonal\. SupposeHHhas ana×ba\\times bsubmatrix whose entries are all11\. Show thata​b≤nab\\leq n\.

DeepSeek\-Prover\-V2\-7B Output \(Buggy\)[⬇](data:text/plain;base64,dGhlb3JlbSBwdXRuYW1fMjAwNV9hNAogICAgKG4gOiDihJUpIChIIDogTWF0cml4IChGaW4gbikgKEZpbiBuKSDihJ0pIChhIGIgOiDihJUpCiAgICAoUyA6IE1hdHJpeCAoRmluIGEpIChGaW4gYikg4oSdKSAobnBvcyA6IG4g4omlIDEpCiAgICAoSGVudHJpZXMgOiDiiIAgaSBqIDogRmluIG4sIEggaSBqID0gMSDiiKggSCBpIGogPSAtMSkKICAgIChIb3J0aG8gOiBILkhhc09ydGhvZ29uYWxSb3dzKQogICAgKGhhYiA6IDEg4omkIGEg4oinIGEg4omkIG4g4oinIDEg4omkIGIg4oinIGIg4omkIG4pCiAgICAoU3N1YiA6IOKIgyAocnJpIDogRmluIGEg4oaSIEZpbiBuKSAoY3JpIDogRmluIGIg4oaSIEZpbiBuKSwKICAgICAgICAgICAgcnJpLkluamVjdGl2ZSDiiKcgY3JpLkluamVjdGl2ZSDiiKcgUyA9IEguc3VibWF0cml4IHJyaSBjcmkpCiAgICAoU2VudHJpZXMgOiDiiIAgKGkgOiBGaW4gYSkgKGogOiBGaW4gYiksIFMgaSBqID0gMSkKICAgIDogYSAqIGIg4omkIG4gOj0gYnkKICBvYnRhaW4g4p+ocnJpLCBjcmksIGhyaW5qLCBoY3JpaiwgaHN1YuKfqSA6PSBTc3ViCiAgaGF2ZSBo4oKBIDogYSDiiaQgbiA6PSBoYWIuMi4xCiAgaGF2ZSBo4oKCIDogYiDiiaQgbiA6PSBoYWIuMi4yLjIKICBoYXZlIGjigoMgOiBhICogYiDiiaQgbiA6PSBieQogICAgY2FsYwogICAgICBhICogYiA9IENhcmRpbmFsLnRvTmF0IChhICogYikgOj0gYnkgc2ltcCBbTmF0LmNhc3RfaW5qXQogICAgICBfIOKJpCBDYXJkaW5hbC50b05hdCAobikgOj0gYnkKICAgICAgICBhcHBseT8gIC0tIEJVRzogaW50cm9kdWNlcyBzeW50aGV0aWMgc29ycnkgd2l0aG91dCBlcnJvcgogICAgICBfID0gbiA6PSBieSBzaW1wIFtOYXQuY2FzdF9pbmpdCiAgZXhhY3QgaOKCgw==)1theorem𝒫\\mathscr\{P\}putnam\_2005\_a42𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\(H𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Matrix𝒫\\mathscr\{P\}\(Fin𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}\(Fin𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(S𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Matrix𝒫\\mathscr\{P\}\(Fin𝒫\\mathscr\{P\}a\)𝒫\\mathscr\{P\}\(Fin𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}\(npos𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}≥\\geq𝒫\\mathscr\{P\}1\)4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(Hentries𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}j𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n,𝒫\\mathscr\{P\}H𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}j𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}∨\\lor𝒫\\mathscr\{P\}H𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}j𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}\-1\)5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(Hortho𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}H\.HasOrthogonalRows\)6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hab𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n\)7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(Ssub𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}\(rri𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}\(cri𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n\),8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}rri\.Injective𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}cri\.Injective𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}S𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}H\.submatrix𝒫\\mathscr\{P\}rri𝒫\\mathscr\{P\}cri\)9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(Sentries𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}\(i𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}a\)𝒫\\mathscr\{P\}\(j𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}b\),𝒫\\mathscr\{P\}S𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}j𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}1\)10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}obtain𝒫\\mathscr\{P\}⟨\\langlerri,𝒫\\mathscr\{P\}cri,𝒫\\mathscr\{P\}hrinj,𝒫\\mathscr\{P\}hcrij,𝒫\\mathscr\{P\}hsub⟩\\rangle𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}Ssub12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}hab\.2\.113𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}hab\.2\.2\.214𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h3𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by15𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}calc16𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}Cardinal\.toNat𝒫\\mathscr\{P\}\(a𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}b\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by𝒫\\mathscr\{P\}simp𝒫\\mathscr\{P\}\[Nat\.cast\_inj\]17𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\_𝒫\\mathscr\{P\}≤\\leq𝒫\\mathscr\{P\}Cardinal\.toNat𝒫\\mathscr\{P\}\(n\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by18𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}apply?𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}19𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\_𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by𝒫\\mathscr\{P\}simp𝒫\\mathscr\{P\}\[Nat\.cast\_inj\]20𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}h3

Problem StatementPutnam 2007\-B4:Letnnbe a positive integer\. Find the number of pairsP,QP,Qof polynomials with real coefficients such that\(P​\(X\)\)2\+\(Q​\(X\)\)2=X2​n\+1\(P\(X\)\)^\{2\}\+\(Q\(X\)\)^\{2\}=X^\{2n\}\+1anddeg⁡P\>deg⁡Q\\deg P\>\\deg Q\.

DeepSeek\-Prover\-V2\-7B Output \(Buggy\)[⬇](data:text/plain;base64,dGhlb3JlbSBwdXRuYW1fMjAwN19iNCAobiA6IOKElSkgKG5wb3MgOiBuID4gMCkgOgogICAgKHsoUCwgUSkgOiAoUG9seW5vbWlhbCDihJ0pIMOXIChQb2x5bm9taWFsIOKEnSkgfAogICAgICBQIF4gMiArIFEgXiAyID0gUG9seW5vbWlhbC5YIF4gKDIgKiBuKSArIDEg4oinCiAgICAgIFAuZGVncmVlID4gUS5kZWdyZWV9Lm5jYXJkID0gKChmdW4gbiDihqYgMiBeIChuICsgMSkpIDog4oSVIOKGkiDihJUpIG4pIDo9IGJ5CiAgaGF2ZSBo4oKBIDog4oiAIG4gOiDihJUsIG4gPiAwIOKGkgogICAgICAoeyhQLCBRKSA6IChQb2x5bm9taWFsIOKEnSkgw5cgKFBvbHlub21pYWwg4oSdKSB8CiAgICAgICAgUCBeIDIgKyBRIF4gMiA9IFBvbHlub21pYWwuWCBeICgyICogbikgKyAxIOKIpwogICAgICAgIFAuZGVncmVlID4gUS5kZWdyZWV9Lm5jYXJkIDog4oSVKSA9IDIgXiAobiArIDEpIDo9IGJ5CiAgICBpbnRybyBuIGhuCiAgICBoYXZlIGggOiDiiIAgbiA6IOKElSwgbiA+IDAg4oaSIC4uLiA6PSBieQogICAgICBpbnRybyBuIGhuCiAgICAgIGhhdmUgaOKCgSA6IC4uLiA6PSBieQogICAgICAgIGhhdmUgaOKCgiA6IC4uLiA6PSBieQogICAgICAgICAgcncgW+KGkCBDYXJkaW5hbC5uYXRDYXN0X2lual0KICAgICAgICAgIGFwcGx5PyAgLS0gQlVHOiBpbnRyb2R1Y2VzIHN5bnRoZXRpYyBzb3JyeSB3aXRob3V0IGVycm9yCiAgICAgICAgZXhhY3RfbW9kX2Nhc3QgaOKCggogICAgICBleGFjdCBo4oKBCiAgICBleGFjdCBoIG4gaG4KICBoYXZlIGjigoIgOiAuLi4gOj0gYnkgYXBwbHkgaOKCgTsgZXhhY3QgbnBvcwogIHNpbXBhIFto4oKCXSB1c2luZyBo4oKC)1theorem𝒫\\mathscr\{P\}putnam\_2007\_b4𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\(npos𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}0\)𝒫\\mathscr\{P\}:2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(\{\(P,𝒫\\mathscr\{P\}Q\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\(Polynomial𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}\(Polynomial𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}\|3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}P𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}Q𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}Polynomial\.X𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}\(2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}∧\\land4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}P\.degree𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}Q\.degree\}\.ncard𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}\(\(fun𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}↦\\mapsto𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\},𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}→\\rightarrow6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(\{\(P,𝒫\\mathscr\{P\}Q\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\(Polynomial𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}×\\times𝒫\\mathscr\{P\}\(Polynomial𝒫\\mathscr\{P\}ℝ\\mathbb\{R\}\)𝒫\\mathscr\{P\}\|7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}P𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}Q𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}Polynomial\.X𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}\(2𝒫\\mathscr\{P\}\*𝒫\\mathscr\{P\}n\)𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}∧\\land8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}P\.degree𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}Q\.degree\}\.ncard𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}intro𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}hn10𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\},𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}\>𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}\.\.\.𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}intro𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}hn12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\.\.\.𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by13𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\.\.\.𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by14𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}rw𝒫\\mathscr\{P\}\[←\\leftarrow𝒫\\mathscr\{P\}Cardinal\.natCast\_inj\]15𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}apply?𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}16𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact\_mod\_cast𝒫\\mathscr\{P\}h217𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}h118𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}h𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}hn19𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}\.\.\.𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by𝒫\\mathscr\{P\}apply𝒫\\mathscr\{P\}h1;𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}npos20𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}simpa𝒫\\mathscr\{P\}\[h2\]𝒫\\mathscr\{P\}using𝒫\\mathscr\{P\}h2

In both cases, theapply?tactic introduces a synthetic sorry that, combined with theCardinaluniverse coercion, triggers the bug\. Lean 4\.9\.0 reports no errors, but the theorems are never actually verified by the kernel\. This bug was fixed in Lean 4\.20\.0\.101010[https://github\.com/leanprover/lean4/pull/8231](https://github.com/leanprover/lean4/pull/8231)

## Appendix EVacuous Hypotheses: An Example from CombiBench

The following example, taken from an earlier version of CombiBench\(Liuet al\.,[2025a](https://arxiv.org/html/2606.29493#bib.bib26)\)\(since corrected\), illustrates how incorrect translation can produce vacuous hypotheses that make a statement trivially provable\.

Problem StatementIMOSL 2011\-C6:Letnnbe a positive integer and letWWbe an infinite periodic word consisting of lettersaaandbb, with minimal periodN\>2nN\>2^\{n\}\. A finite nonempty wordUUis*ubiquitous*if all four wordsU​aUa,U​bUb,a​UaU, andb​UbUappear inWW\. Prove that there are at leastnnubiquitous finite nonempty words\.

CombiBench Formalization \(Vacuous Hypotheses\)[⬇](data:text/plain;base64,ZGVmIGFwcGVhcnMgKFcgOiDihKQg4oaSIEZpbiAyKSAoVSA6IM6jIG4sIEZpbiBuIOKGkiBGaW4gMikgOiBQcm9wIDo9CiAg4oiDIGssIOKIgCBpIDogRmluIFUuMSwgVS4yIGkgPSBXIChrICsgaSkKCmRlZiB1YmlxdWl0b3VzIChXIDog4oSkIOKGkiBGaW4gMikgKFUgOiDOoyBuLCBGaW4gbiDihpIgRmluIDIpIDogUHJvcCA6PQogIGFwcGVhcnMgVyDin6hVLjEgKyAxLCBGaW4uc25vYyBVLjIgMOKfqSDiiKcKICBhcHBlYXJzIFcg4p+oVS4xICsgMSwgRmluLnNub2MgVS4yIDHin6kg4oinCiAgYXBwZWFycyBXIOKfqFUuMSArIDEsIEZpbi5jb25zIDAgVS4y4p+pIOKIpwogIGFwcGVhcnMgVyDin6hVLjEgKyAxLCBGaW4uY29ucyAxIFUuMuKfqQoKdGhlb3JlbSBpbW9zbF8yMDExX2M2IChXIDog4oSkIOKGkiBGaW4gMikgKG4gOiDihJUrKSAoTiA6IOKElSkgKGhOIDogMiBeIG4uMSA8IE4pCiAgICAoaFcgOiBGdW5jdGlvbi5QZXJpb2RpYyBXIE4pCiAgICAoaFcnIDog4oiAIE4nIDwgTiwgwqxGdW5jdGlvbi5QZXJpb2RpYyBXIE4nKSA6ICAtLSBwcm9ibGVtYXRpYyEKICAgIOKIgyAoeCA6IEZpbiBuIOKGqiAozqMgaywgRmluIGsg4oaSIEZpbiAyKSksCiAgICAgICjiiIAgaSwgKHggaSkuMSDiiaAgMCkg4oinICjiiIAgaSwgdWJpcXVpdG91cyBXICh4IGkpKSA6PSBieQogIHNvcnJ5)1def𝒫\\mathscr\{P\}appears𝒫\\mathscr\{P\}\(W𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}\(U𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Σ\\Sigma𝒫\\mathscr\{P\}n,𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Prop𝒫\\mathscr\{P\}:=2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}k,𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}U\.1,𝒫\\mathscr\{P\}U\.2𝒫\\mathscr\{P\}i𝒫\\mathscr\{P\}=𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}\(k𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}i\)34def𝒫\\mathscr\{P\}ubiquitous𝒫\\mathscr\{P\}\(W𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}\(U𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Σ\\Sigma𝒫\\mathscr\{P\}n,𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Prop𝒫\\mathscr\{P\}:=5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}appears𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}⟨\\langleU\.1𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1,𝒫\\mathscr\{P\}Fin\.snoc𝒫\\mathscr\{P\}U\.2𝒫\\mathscr\{P\}0⟩\\rangle𝒫\\mathscr\{P\}∧\\land6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}appears𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}⟨\\langleU\.1𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1,𝒫\\mathscr\{P\}Fin\.snoc𝒫\\mathscr\{P\}U\.2𝒫\\mathscr\{P\}1⟩\\rangle𝒫\\mathscr\{P\}∧\\land7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}appears𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}⟨\\langleU\.1𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1,𝒫\\mathscr\{P\}Fin\.cons𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}U\.2⟩\\rangle𝒫\\mathscr\{P\}∧\\land8𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}appears𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}⟨\\langleU\.1𝒫\\mathscr\{P\}\+𝒫\\mathscr\{P\}1,𝒫\\mathscr\{P\}Fin\.cons𝒫\\mathscr\{P\}1𝒫\\mathscr\{P\}U\.2⟩\\rangle910theorem𝒫\\mathscr\{P\}imosl\_2011\_c6𝒫\\mathscr\{P\}\(W𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℤ\\mathbb\{Z\}𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)𝒫\\mathscr\{P\}\(n𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\+\)𝒫\\mathscr\{P\}\(N𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}ℕ\\mathbb\{N\}\)𝒫\\mathscr\{P\}\(hN𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}n\.1𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}N\)11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hW𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Function\.Periodic𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}N\)12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(hW’𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}∀\\forall𝒫\\mathscr\{P\}N’𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}N,𝒫\\mathscr\{P\}¬\\negFunction\.Periodic𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}N’\)𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}13𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}∃\\exists𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}n𝒫\\mathscr\{P\}↪\\hookrightarrow𝒫\\mathscr\{P\}\(Σ\\Sigma𝒫\\mathscr\{P\}k,𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}k𝒫\\mathscr\{P\}→\\rightarrow𝒫\\mathscr\{P\}Fin𝒫\\mathscr\{P\}2\)\),14𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}\(∀\\forall𝒫\\mathscr\{P\}i,𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}i\)\.1𝒫\\mathscr\{P\}≠\\neq𝒫\\mathscr\{P\}0\)𝒫\\mathscr\{P\}∧\\land𝒫\\mathscr\{P\}\(∀\\forall𝒫\\mathscr\{P\}i,𝒫\\mathscr\{P\}ubiquitous𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}\(x𝒫\\mathscr\{P\}i\)\)𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by15𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}sorry

##### The problem\.

The hypothesishW’attempts to encode thatNNis the*minimal*period: no smaller valueN′<NN^\{\\prime\}<Nshould also be a period\. However,Function\.Periodic W 0is*definitionally true*in Lean—it unfolds to∀z,W​\(z\+0\)=W​\(z\)\\forall z,\\,W\(z\+0\)=W\(z\), which reduces to∀z,W​\(z\)=W​\(z\)\\forall z,\\,W\(z\)=W\(z\)and is provable byrfl\.

Sincen≥1n\\geq 1implies2n≥22^\{n\}\\geq 2, andN\>2nN\>2^\{n\}, we haveN≥3N\\geq 3, so0<N0<N\. ThereforehW’ 0yields¬Function\.Periodic W 0\\neg\\texttt\{Function\.Periodic W 0\}, which contradicts the definitional truth ofFunction\.Periodic W 0\.

##### The exploit\.

A model can deriveFalsefrom the hypotheses and prove anything viaexfalso:

Model\-Generated Proof \(Exploiting Vacuous Hypotheses\)[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9zbF8yMDExX2M2IC4uLiA6PSBieQogIC0tIERlcml2ZSBGYWxzZTogaFcnIHNheXMgUGVyaW9kaWMgVyAwIGlzIGZhbHNlLCBidXQgaXQncyBkZWZpbml0aW9uYWxseSB0cnVlCiAgaGF2ZSBoX2NvbnRyYSA6IEZhbHNlIDo9IGJ5CiAgICBoYXZlIGjigoAgOiAwIDwgTiA6PSBieQogICAgICBoYXZlIDogMiBeIG4uMSDiiaUgMiA6PSBOYXQub25lX2xlX3BvdyBuLjEgMiAoYnkgbm9ybV9udW0pCiAgICAgIG9tZWdhCiAgICBoYXZlIGjigoEgOiDCrEZ1bmN0aW9uLlBlcmlvZGljIFcgMCA6PSBoVycgMCBo4oKACiAgICBoYXZlIGjigoIgOiBGdW5jdGlvbi5QZXJpb2RpYyBXIDAgOj0gZnVuIHogPT4gcmZsICAtLSBkZWZpbml0aW9uYWxseSB0cnVlIQogICAgZXhhY3QgaOKCgSBo4oKCCiAgLS0gQ29uY2x1ZGUgYW55dGhpbmcgZnJvbSBGYWxzZQogIGV4ZmFsc28KICBleGFjdCBoX2NvbnRyYQ==)1theorem𝒫\\mathscr\{P\}imosl\_2011\_c6𝒫\\mathscr\{P\}\.\.\.𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by2𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}3𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h\_contra𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}False𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by4𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h0𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}<𝒫\\mathscr\{P\}N𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}by5𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}^𝒫\\mathscr\{P\}n\.1𝒫\\mathscr\{P\}≥\\geq𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}Nat\.one\_le\_pow𝒫\\mathscr\{P\}n\.1𝒫\\mathscr\{P\}2𝒫\\mathscr\{P\}\(by𝒫\\mathscr\{P\}norm\_num\)6𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}omega7𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h1𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}¬\\negFunction\.Periodic𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}hW’𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}h08𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}have𝒫\\mathscr\{P\}h2𝒫\\mathscr\{P\}:𝒫\\mathscr\{P\}Function\.Periodic𝒫\\mathscr\{P\}W𝒫\\mathscr\{P\}0𝒫\\mathscr\{P\}:=𝒫\\mathscr\{P\}fun𝒫\\mathscr\{P\}z𝒫\\mathscr\{P\}=\>𝒫\\mathscr\{P\}rfl𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}9𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}h1𝒫\\mathscr\{P\}h210𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}11𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exfalso12𝒫\\mathscr\{P\}𝒫\\mathscr\{P\}exact𝒫\\mathscr\{P\}h\_contra

##### Lesson\.

This is not a Lean bug, the kernel correctly verifies thatFalseimplies anything\. The issue is a*formalization defect*: the minimality condition was incorrectly translated, producing unsatisfiable hypotheses\. The correct formalization should excludeN′=0N^\{\\prime\}=0\(e\.g\.,∀N′,0<N′<N→¬Periodic​\(W,N′\)\\forall N^\{\\prime\},\\,0<N^\{\\prime\}<N\\to\\neg\\texttt\{Periodic\}\(W,N^\{\\prime\}\)\)\. Such issues are invisible to typechecking and require either careful human review or attempting to construct proofs during benchmark development\.

## Appendix FAutomated Checker Details

We implement 12 static checkers targeting common Lean semantic hazards\. All checkers use*semantic guard proving*\(Paulinoet al\.,[2024](https://arxiv.org/html/2606.29493#bib.bib36)\): rather than pattern\-matching on hypothesis syntax, we attempt to prove guard conditions using Lean’sassumption,simp, andomegatactics\. This catches guards that are implied by other hypotheses \(e\.g\.,0 < bimpliesb≠\\neq0\)\.

CheckerCategoryDetectionGuard MethodNatSubtractionLean Technicala \- bonNat\(saturating subtraction\)Provesb≤\\leqaDivisionByZeroLean Technicala / bwithout divisor guardProvesb≠\\neq0ModuloByZeroLean Technicala % bwithout divisor guardProvesb≠\\neq0IntDivTruncationLean TechnicalInteger division that truncates \(e\.g\.,1/4\)Literal analysisIntToNatLean TechnicalInt\.toNatwithout non\-negativity guardProves0≤\\leqxAnalyticDomainLean TechnicalInv\.inv,sqrt,logwithout domain guardsProvesx≠\\neq0,0≤\\leqx,0 < xVacuousCheckSpecificationContradictory hypotheses \(can proveFalse\)AttemptsFalseproofEmptyDomainSpecificationQuantification over empty types \(Fin 0,Empty\)Type emptiness checkUnusedBinderSpecification∀\\forallx, Pwherexdoes not appear inPFree variable analysisAxiomCheckerVerificationUser\-definedaxiomasserting aPropDeclaration typeListRangeReviewList\.range,Finset\.range\(0\-indexed\)Flagged for manual reviewTable 9:Full list of automated checkers\. “Lean Technical” checkers detect semantic hazards from Lean’s totalized arithmetic\. “Specification” checkers flag potential formalization errors\. “Verification” checkers detect proof shortcuts\. “Review” checkers flag patterns requiring human judgment\.##### Semantic guard proving\.

For arithmetic hazards \(division, subtraction, domain guards\), we do not rely on syntactic pattern matching\. Instead, we construct the required guard goal \(e\.g\.,b≠\\neq0\) and attempt to prove it using Lean’s tactic machinery:

1. 1\.assumption: Check if the guard is directly available in the local context\.
2. 2\.simp: Apply simplification lemmas \(e\.g\.,Nat\.succ n≠\\neq0\)\.
3. 3\.omega: Use linear arithmetic to derive the guard from other hypotheses\.

This approach catches guards that are implied but not syntactically present \(e\.g\.,0 < bimpliesb≠\\neq0\)\.

##### Checker outputs\.

Each checker reports:

- •The flagged expression and its location
- •Whether a guard was found, and how it was proven \(assumption,simp, oromega\)
- •A suggested fix

### F\.1Soundness Checkers

These checkers detect specifications that are fundamentally broken\.

##### Counterexample\.

The most direct soundness check: attempts to find concrete values that satisfy the hypotheses but violate the conclusion\. Usesdecideandnative\_decidefor decidable propositions, and enumerates small finite domains \(e\.g\., integers in\[−10,10\]\[\-10,10\], small lists\)\. A successful counterexample definitively proves the specification is wrong\. For example, a theorem claiming “∀n,f​\(n\)\>0\\forall n,\\,f\(n\)\>0” is refuted by exhibitingn=5n=5wheref​\(5\)=0f\(5\)=0\.

##### Vacuous Theorem\.

Detects theorems with unsatisfiable hypotheses, making them trivially true but mathematically useless\. For implicationsH→CH\\to C, attempts to prove¬H\\neg Husingomegaandsimp\. Catches specifications like:

```
theorem broken (x : Z) (h1 : x < 0) (h2 : x > 0) : P x
```

This is provable \(by contradiction onh1,h2h\_\{1\},h\_\{2\}\) but proves nothing meaningful—the hypotheses can never be satisfied\.

##### Unsound Axiom\.

Flagsaxiomdeclarations andsorryin proofs\. While Mathlib relies on standard axioms \(propext,Quot\.sound,Classical\.choice\), benchmark problems should not introduce new axioms\. An axiom asserts a fact without proof, potentially masking specification errors\. For example:

```
axiom sol_prop {a : R} (ha : -1 < a) : -1 < -a / (1 + a)
```

### F\.2Totalization Checkers

These checkers detect misuse of Lean’s totalized functions, where mathematically undefined operations return default values\.

##### Division by Zero\.

Detects division \(a / b\), modulo \(a % b\), and inverse \(b\-1\) operations\. For each occurrence, constructs the goalb≠\\neq0and attempts proof using the local context\. In Lean,a / 0 = 0by definition, so unguarded division can silently produce wrong values\. Supports LLM verification for cases where guards exist in structures or subtypes\.

##### Truncated Natural Subtraction\.

Natural number subtraction in Lean is truncated:2 \- 3 = 0\. The checker flagsa \- bfora b :ℕ\\mathbb\{N\}and attempts to proveb≤\\leqa\. This catches specifications that silently produce zero instead of negative values, particularly in loop bounds and index calculations\.

##### Analytic Domain Totalization\.

Mathematical functions in Mathlib are totalized with default values outside their natural domains:

- •Real\.sqrt x = 0forx<0x<0
- •Real\.log x = 0forx≤0x\\leq 0

The checker flags these functions and attempts to prove domain membership \(e\.g\.,0≤\\leqxforsqrt\)\.

##### Integer Division Truncation\.

Flags integer division \(a / bfora b :ℤ\\mathbb\{Z\}\) in theorem statements\. Unlike real division, integer division truncates toward zero, which may not match the intended mathematical semantics\. This is informational—not all uses are errors\.

### F\.3Specification Quality Checkers

##### Unused Quantified Variable\.

Detects∀\\forallx, Por∃\\existsx, Pwherexdoes not appear free inP\. Common causes include copy\-paste errors, vestigial parameters from problem evolution, or incomplete formalization\. Example:

```
theorem usa2024_p2 (n : N) : IsLeast {k | ...} 100  -- n unused!
```

##### Zero\-Indexed Range\.

Reports uses ofFin norFinset\.range nstarting from index 0 when the problem statement uses 1\-indexed notation \(“fori=1,2,…,ni=1,2,\\ldots,n”\)\. This is informational, as the discrepancy may be intentional\.

### F\.4Implementation

Checkers are implemented as Lean 4 metaprograms that traverse elaborated expression trees\. The pipeline:

1. 1\.Parse Lean source and elaborate toExpr
2. 2\.Traverse subexpressions, matching patterns for each checker category
3. 3\.For guard\-based checkers, construct the guard as a goal and run tactic proof
4. 4\.Collect findings where pattern matches but guard proof fails

Guard proving uses a tactic sequence:omega\(linear arithmetic overℤ\\mathbb\{Z\}andℕ\\mathbb\{N\}\),assumption\(direct hypothesis match\),simp \[\*\]\(simplification with local lemmas\)\. This discharges approximately 60% of valid guards automatically\.

## Appendix GLLM Verification Details

### G\.1Motivation

Static guard proving fails in several scenarios:

- •Structure guards: Constraints defined in structures \(e\.g\.,structure IsValid where pos : 0 < x\) are not visible when checking expressions using the structure
- •Subtype constraints: Types likePosReal := \{x :ℝ\\mathbb\{R\}// 0 < x\}encode guards in the type, but the checker sees only the base type
- •Non\-local reasoning: Guards may require chaining through multiple definitions
- •Naming conventions: Hypothesis names likehposorhnesuggest guards but aren’t machine\-readable

LLMs, trained on mathematical code, can recognize these patterns and determine whether a semantic guard exists even when the static prover cannot find it\.

### G\.2Evaluation Setup

We manually labeled 55 findings across three checker categories \(Division by Zero, Nat Subtraction, Analytic Domain\) from ProverBench\. Each finding was classified as:

- •True Positive: No guard exists; the finding represents a real issue
- •False Positive: A guard exists but wasn’t recognized by static analysis

Ground truth distribution: 42 true positives \(76%\), 13 false positives \(24%\)\.

### G\.3Model Comparison

Table 10:Full model comparison on 55 labeled examples\. FP = false positives introduced, FN = false negatives \(missed true positives\)\.DeepSeek\-V3 achieves perfect recall but low precision—it rarely filters anything, defeating the purpose\. The other three models achieve similar accuracy \(∼\\sim82%\), with GPT\-5\.2 having highest precision \(fewest false positives\) and Gemini Flash offering the best cost\-effectiveness\.

### G\.4Per\-Checker Accuracy \(GPT\-5\.2\)

Table 11:GPT\-5\.2 accuracy breakdown by checker category\.
### G\.5Production Results: ProverBench

Applying GPT\-5\.2 filtering to ProverBench \(325 problems\):

Table 12:LLM filtering results on ProverBench by category\.Manual verification confirmed that all known true positives were preserved after filtering\.

### G\.6Limitations

- •Context window: Very long proofs may exceed token limits, requiring truncation
- •Subtype reasoning: Models occasionally miss thatx : \{y // P y\}impliesP x
- •Non\-determinism: Even at temperature 0, API responses may vary slightly across runs
- •Cost at scale: Full verification of large datasets requires budget planning \($0\.09–$0\.42 per 55 examples depending on model\)
- •Categories not covered: LLM verification is only applied to guard\-based checkers; Counterexample, Vacuous, and Unsound Axiom findings are deterministic and not filtered

## Appendix HLLM\-Assisted Semantic Audit: Full Results

This appendix provides detailed results from the LLM\-assisted semantic audit described in Section[4\.2](https://arxiv.org/html/2606.29493#S4.SS2)\.

### H\.1Extended Model Comparison

Table[13](https://arxiv.org/html/2606.29493#A8.T13)compares all models tested, including both base and extended reasoning variants\.

Table 13:LLM semantic audit performance across all datasets \(92 problems, 552 classifications\)\. Extended reasoning consistently improves accuracy at higher cost\.Extended reasoning provides \+10–17% accuracy improvement but at 3–17×\\timeshigher cost\. Gemini Flash without reasoning offers the best cost\-effectiveness for initial screening\.

### H\.2Per\-Category Performance

Table[14](https://arxiv.org/html/2606.29493#A8.T14)shows F1 scores by error category for all model variants\.

Table 14:Per\-category F1 scores\. Formalization errors—requiring semantic judgment about whether encodings preserve intent—remain challenging across all models\.The 3×\\timesgap in F1 between specification errors \(0\.51\) and formalization errors \(0\.18\) confirms that these categories require fundamentally different detection strategies—matching our taxonomy distinction\.

### H\.3Cost Analysis

Table 15:API costs for LLM\-assisted audit \(92 problems×\\times6 categories = 552 classifications\)\.For production use at scale, we recommend starting with base models \(Gemini Flash at $0\.48 per 92 problems\) and reserving extended reasoning for problems flagged as uncertain\.

Few\-shot examples were drawn from problems not in the evaluation set and manually verified for correctness\. Full prompts are available in our code release\.

For production use at scale, we recommend starting with base models \(Gemini Flash at $0\.48 per 92 problems\) and reserving extended reasoning for problems flagged as uncertain\.

### H\.4Prompt Structure

Each evaluation uses a structured prompt containing:

1. 1\.System instruction defining the classification task
2. 2\.Error category definition and detection criteria from our taxonomy
3. 3\.Three few\-shot examples \(both positive and negative cases\)
4. 4\.The problem to evaluate \(NL statement \+ Lean formalization\)
5. 5\.Output format specification \(structured JSON with classification and explanation\)

Few\-shot examples were drawn from problems not in the evaluation set and manually verified for correctness\.

#### H\.4\.1Shared Preamble \(System Prompt\)

All six category prompts share a common preamble:

Shared Preamble \(System Prompt\)Role:You are an expert auditor for NL→\\toLean 4 formalizations\.Input:\(1\) Natural language problem statement \(NL\); \(2\) Lean 4 code snippet \(Lean\)\. Focus on the*main theorem/definition statement*that encodes the NL\. Ignore the proof \(by sorryetc\.\)\.Task:For ONE specific error category \(given below\), decide whether the Lean statement has an error of that category relative to the NL problem\.Rules:1\.Output MUST be valid JSON \(no markdown, no extra keys\)\.2\.Say NO if the formalization is correct for this category, even if other categories might have issues\.3\.Say NO if there is no semantic error at all\.4\.Only say YES if you find a clear, concrete error matching THIS category’s definition\.5\.If not confident, setNeedsReview = "YES"\.6\.DetailTagsmust be chosen ONLY from the allowed list\.Output format \(JSON\): Verdict:"YES"or"NO"Explanation: 1–3 sentencesDetailTags: array of stringsNeedsReview:"YES"or"NO"

#### H\.4\.2Category Prompts

Each category prompt appends a definition, boundary rules, allowed detail tags, and three few\-shot examples \(one YES, one NO with a different\-category error, one NO with no error\)\.

Prompt 1:problem\_statement\_errorDefinition:The NL problem itself is ambiguous, ill\-posed, unformalizable, or false as stated\. Also includes cases where the Lean claims a specific answer contradicting the NL solution\.Allowed tags:ambiguity\_or\_unformalizable,wrong\_question,incomplete\_statement,unprovable\_problem,literal\_mismatch,otherExample 1\(Verdict: YES — NL constraints make problem unsolvable\)NL:Find quadratic polynomialsf​\(x\)=a​x2\+b​x\+cf\(x\)=ax^\{2\}\+bx\+cwherea,b,ca,b,care positive integers,p<qp<qare primes,f​\(p\)=f​\(q\)=17f\(p\)=f\(q\)=17,f​\(p\+q\)=47f\(p\+q\)=47\.Lean:theorem omni\_theorem\_2830 : \(finprod x in \{x \|∃\\existsa b c p q : Nat, a \> 0∧\\landp\.Prime∧\\landq\.Prime∧\\land…\}, x\) % 100 = 71 := by sorry Verdict:YES\. Solving the constraints forcesb=−a​\(p\+q\)<0b=\-a\(p\+q\)<0; no solutions exist with positivebb\. Tag:unprovable\_problem\.Example 2\(Verdict: NO — error isdomain\_mismatch\)NL:Find all positive integersk,nk,nsuch that7k−3n∣k4\+n27^\{k\}\-3^\{n\}\\mid k^\{4\}\+n^\{2\}\. Answer:\(k,n\)=\(2,4\)\(k,n\)=\(2,4\)\.Lean:theorem olymid\_ref\_base\_3054 \(k n : Nat\) : k \> 0∧\\landn \> 0∧\\land7ˆk \- 3ˆn∣\\midkˆ4 \+ nˆ2↔\\leftrightarrow\(k = 2∧\\landn = 4\) := by sorry Verdict:NO\. The NL problem is well\-posed; the issue is Nat subtraction truncation \(domain\_mismatch\)\.Example 3\(Verdict: NO — correct\)NL:Use the pigeonhole principle to prove that a graph of ordern≥2n\\geq 2always has two vertices of the same degree\.Lean:theorem brualdi\_ch11\_5 \{V : Type\*\} \(n : Nat\) \(h\_n : n≥\\geq2\) \(G : SimpleGraph \(Fin n\)\) \[DecidableRel G\.Adj\] :∃\\existsv1 v2, v1≠\\neqv2∧\\landG\.degree v1 = G\.degree v2 := by sorry Verdict:NO\. The NL is well\-posed and the Lean statement correctly formalizes it\. No error\.Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

Prompt 2:specification\_errorDefinition:The mathematical specification is missing, extra, or incorrect assumptions, constraints, or scope\.Allowed tags:missing\_hypothesis,extra\_hypothesis,distinctness\_missing,incomplete\_spec,incorrect\_spec,oversimplified\_spec,base\_case\_missing,division\_by\_zero\_risk,uniqueness\_missing,otherBoundary:Wrong type→\\todomain\_mismatch\. Quantifier/indexing→\\toquantifier\_indexing\_mismatch\.Example 1\(Verdict: YES — missing prime constraint\)NL:Prove that a group of order 312 has a normal Sylowpp\-subgroup for some primeppdividing its order\.Lean:theorem exercise\_4\_5\_14 \{G : Type\*\} \[Group G\] \[Fintype G\] \(hG : card G = 312\) :∃\\exists\(p : Nat\) \(P : Sylow p G\), P\.Normal := sorry Verdict:YES\. NL requires “primeppdividing its order” but Lean only has∃p\\exists\\,pwithoutp\.Primeorp∣\\midcard G\. Trivialp=1p=1satisfies the Lean statement\. Tag:incomplete\_spec\.Example 2\(Verdict: NO — error isdefinition\_mismatch\)NL:What is the smallest integernnsuch that1/2<n/91/2<n/9? Answer: 5\.Lean:theorem omni\_theorem\_2926 : IsLeast \{n \| 1/2 < n/9\} 5 := by sorry Verdict:NO\. The specification is correct; the issue is that1/2andn/9use Nat division giving 0 \(definition\_mismatch\)\.Example 3\(Verdict: NO — correct\)NL:SupposeUUis a subspace ofVV\. ProveU⟂=\{0\}U^\{\\perp\}=\\\{0\\\}iffU=VU=V\.Lean:theorem exercise\_6\_16 \{K V : Type\*\} \[RCLike K\] \[NormedAddCommGroup V\] \[InnerProductSpace K V\] \{U : Submodule K V\} : U\.orthogonal =⊥\\botiff U =⊤\\top:= sorry Verdict:NO\. All necessary hypotheses are present\. No error\.Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

Prompt 3:formalization\_errorDefinition:The spec is clear, but the Lean encoding does not match due to translation choices \(wrong connectives, contradictory premises, structural mismatch\)\.Allowed tags:goal\_mismatch,missing\_subgoal,premise\_translation\_error,goal\_translation\_error,connective\_mismatch,contradictory\_premises,otherBoundary:Wrong type→\\todomain\_mismatch\. Wrong concept→\\todefinition\_mismatch\. Indexing issues→\\toquantifier\_indexing\_mismatch\.Example 1\(Verdict: YES — contradictory premises\)NL:Leta1<a2<⋯<ana\_\{1\}<a\_\{2\}<\\cdots<a\_\{n\}be positive reals withan\+1=a1a\_\{n\+1\}=a\_\{1\}\(cyclic\)\. Prove inequality\.Lean:theorem olymid\_ref\_base\_6282 \{n : Nat\} \(a : Fin \(n\+1\)→\\toReal\) \(ha : StrictMono a\) \(han : a n = a 0\) : …:= by sorry Verdict:YES\.StrictMono ameansa​0<a​1<⋯<a​na\\,0<a\\,1<\\cdots<a\\,n, buthansaysa​n=a​0a\\,n=a\\,0\. Premises are contradictory\. Tag:contradictory\_premises\.Example 2\(Verdict: NO — error isquantifier\_indexing\_mismatch\)NL:Prove\(∑j=1naj​bj\)2≤\(∑j=1nj​aj2\)​\(∑j=1nbj2/j\)\\bigl\(\\sum\_\{j=1\}^\{n\}a\_\{j\}b\_\{j\}\\bigr\)^\{2\}\\leq\\bigl\(\\sum\_\{j=1\}^\{n\}ja\_\{j\}^\{2\}\\bigr\)\\bigl\(\\sum\_\{j=1\}^\{n\}b\_\{j\}^\{2\}/j\\bigr\)\.Lean:theorem exercise\_6\_3 \{n : Nat\} \(a b : Fin n→\\toReal\) : \(∑\\sumi, a i \* b i\)ˆ2≤\\leq…:= sorry Verdict:NO\. Logical structure is correct; the issue isj=1\.\.nj=1\.\.nvs\.i=0\.\.n−1i=0\.\.n\{\-\}1indexing \(quantifier\_indexing\_mismatch\)\.Example 3\(Verdict: NO — correct\)NL:Every closed set in a separable metric space is the union of a perfect set and a countable set\.Lean:theorem exercise\_2\_28 \(X : Type\*\) \[MetricSpace X\] \[SeparableSpace X\] \(A : Set X\) \(hA : IsClosed A\) :∃\\existsP1 P2, A = P1∪\\cupP2∧\\landIsPerfect P1∧\\landSet\.Countable P2 := sorry Verdict:NO\. The Lean statement correctly encodes the NL\. No formalization error\.Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

Prompt 4:domain\_mismatchDefinition:The Lean statement uses the wrong carrier type or domain, changing meaning \(e\.g\.,Natvs\.Int,Fin nvs\.1\.\.n1\.\.n, truncating subtraction/division\)\.Allowed tags:type\_mismatch,domain\_of\_variables\_mismatch,truncation\_issue,otherBoundary:Missing constraints with correct domain→\\tospecification\_error\.Example 1\(Verdict: YES — Nat subtraction truncates\)NL:P=t2−12​t\+180P=t^\{2\}\-12t\+180where1≤t≤61\\leq t\\leq 6\. Find day whenP=160P=160\.Lean:theorem u\_math\_684 \(t : Nat\) \(ht : 1≤\\leqt∧\\landt≤\\leq6\) : let P := tˆ2 \- 12\*t \+ 180; P = 160↔\\leftrightarrowt = 2 := by sorry Verdict:YES\. Uses Nat subtraction: att=2t=2, mathematicallyP=4−24\+180=160P=4\-24\+180=160, but inℕ\\mathbb\{N\},4−244\-24truncates to0, givingP=180≠160P=180\\neq 160\. Tag:truncation\_issue\.Example 2\(Verdict: NO — error isspecification\_error\)NL:For anyn∈ℕ∗n\\in\\mathbb\{N\}^\{\*\}\(positive integers\), if∑d∣nad=2n\\sum\_\{d\\mid n\}a\_\{d\}=2^\{n\}, proven∣ann\\mid a\_\{n\}\.Lean:theorem algebra\_56552 \{a : Nat→\\toNat\} \(ha :∀\\foralln,∑\\sumd in n\.divisors, a d = 2ˆn\) :∀\\foralln, n∣\\mida n := by sorry Verdict:NO\. The domainNat→\\toNatis appropriate; the issue is that NL saysn∈ℕ∗n\\in\\mathbb\{N\}^\{\*\}but Lean includesn=0n=0\(specification\_error\)\.Example 3\(Verdict: NO — correct\)NL:Find smallest positivennwhere1\!⋅2\!​⋯​\(n−1\)\!\>\(n\!\)21\!\\cdot 2\!\\cdots\(n\{\-\}1\)\!\>\(n\!\)^\{2\}\.Lean:theorem olymid\_ref\_base\_5274 : IsLeast \{n : Nat \| 0 < n∧\\land∏\\prodi in Finset\.Icc 1 \(n\-1\), i \! \> \(n \!\)ˆ2\} 8 := by sorry Verdict:NO\. DomainNatis correct for factorials; product rangeIcc 1 \(n\-1\)correctly gives1\!⋅2\!​⋯​\(n−1\)\!1\!\\cdot 2\!\\cdots\(n\{\-\}1\)\!\. No error\.Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

Prompt 5:definition\_mismatchDefinition:Lean objects do not represent the intended math notion \(wrong operator, wrong constant, wrong library concept, misuse of API\)\.Allowed tags:misuse\_of\_concept,wrong\_operator,wrong\_constant,library\_usage\_error,incorrect\_function\_choice,paper\_vs\_lean\_semantics,encoding\_issue,otherBoundary:Wrong type→\\todomain\_mismatch\. Missing assumptions→\\tospecification\_error\.Example 1\(Verdict: YES — indefinite vs\. definite integral\)NL:Compute∫−1/\(3​sin6⁡\(x/3\)\)​d​x\\int\-1/\(3\\sin^\{6\}\(x/3\)\)\\,dx\. Answer involves\+C\+C\.Lean:theorem u\_math\_921 :∫\\intx, \-1 / \(3 \* sin \(x/3\)ˆ6\) = \.\.\. \+ C := by sorry Verdict:YES\. NL asks for an indefinite integral \(antiderivative\+C\+C\), but Lean’s∫\\intx, f xis a definite Lebesgue integral;CCappears as a free variable\. Tag:misuse\_of\_concept\.Example 2\(Verdict: NO — error isquantifier\_indexing\_mismatch\)…Example 3\(Verdict: NO — correct\)…Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

Prompt 6:quantifier\_indexing\_mismatchDefinition:Bug in quantifiers, bounds, indexing, or variable scope \(off\-by\-one, wrong range, free vs\. bound variable\)\.Allowed tags:quantifier\_mismatch,indexing\_mismatch,bound\_mismatch,variable\_mismatch,otherBoundary:Connective issues→\\toformalization\_error\. Missing constraints→\\tospecification\_error\. Wrong types→\\todomain\_mismatch\.Example 1\(Verdict: YES — 0\-indexed vs\. 1\-indexed\)NL:Prove\(∑j=1naj​bj\)2≤\(∑j=1nj​aj2\)​\(∑j=1nbj2/j\)\\bigl\(\\sum\_\{j=1\}^\{n\}a\_\{j\}b\_\{j\}\\bigr\)^\{2\}\\leq\\bigl\(\\sum\_\{j=1\}^\{n\}ja\_\{j\}^\{2\}\\bigr\)\\bigl\(\\sum\_\{j=1\}^\{n\}b\_\{j\}^\{2\}/j\\bigr\)\.Lean:theorem exercise\_6\_3 \{n : Nat\} \(a b : Fin n→\\toReal\) : \(∑\\sumi, a i \* b i\)ˆ2≤\\leq\(∑\\sumi : Fin n, i \* a iˆ2\) \* \(∑\\sumi, b iˆ2 / i\) := sorry Verdict:YES\. NL sumsj=1\.\.nj=1\.\.nwith weightsjjand1/j1/j\. Lean usesFin n\(0\.\.n−10\.\.n\{\-\}1\); ati=0i=0, divides by zero\. Tag:indexing\_mismatch\.Example 2\(Verdict: NO — error isdefinition\_mismatch\)…Example 3\(Verdict: NO — correct\)…Input:\{\{PROBLEM\_NL\}\}and\{\{LEAN\_CODE\}\}are substituted at runtime\. Output: JSON only\.

### H\.5Static Checker False Positive Verification Prompts

Each static checker category has a specialized LLM prompt with domain\-specific knowledge for determining whether a warning is a true or false positive\.

Verification Prompt: Modulo Edge CaseRole:Lean 4 and Mathlib expert specializing in number theory formalization\.Background\.In Lean 4/Mathlib,n % 0 = nby definition \(not undefined\)\. A static analyzer flagged a modulo operation without an explicit≠\\neq0guard for the divisor\.Task\.Determine if the divisor can be proven non\-zero from the theorem’s hypotheses\.Domain knowledge:•Nat\.Prime pimpliesp≥2p\\geq 2, thereforep≠0p\\neq 0•Prime p\(for integers\) impliesp≠0p\\neq 0•p\.Primeis notation forNat\.Prime p•Any prime powerpkp^\{k\}wherePrime pis also non\-zero•Odd palone does*not*implyp≠0p\\neq 0Input:\{theorem\}and\{warning\}are substituted at runtime\.Output format: VERDICT: \[TRUE\_POSITIVE\|FALSE\_POSITIVE\] REASON: \[one sentence explanation\]

Verification Prompt: Nat SubtractionRole:Lean 4 and Mathlib expert specializing in natural number arithmetic\.Background\.In Lean 4, natural subtraction is truncated:a \- b = 0whena < b\. A static analyzer flagged a subtraction without an explicitb≤\\leqaguard\.Task\.Determine ifb≤\\leqacan be proven from the theorem’s hypotheses or is algebraically always true\.Domain knowledge:•For alln : Nat:nk≤nmn^\{k\}\\leq n^\{m\}whenk≤mk\\leq mandn≥1n\\geq 1•\(n\+1\)k\>nk\(n\+1\)^\{k\}\>n^\{k\}for alln,kn,kwithk\>0k\>0•n≤2​nn\\leq 2n,n≤n2\+nn\\leq n^\{2\}\+n,n≤n​\(n\+1\)n\\leq n\(n\+1\)for allnn•Nat\.Prime pimpliesp≥2p\\geq 2, so1≤p1\\leq pand2≤p2\\leq p•k\>0k\>0impliesk≥1k\\geq 1fork : Nat•n≥1n\\geq 1directly gives the guard forn \- 1Input:\{theorem\}and\{warning\}are substituted at runtime\.Output format: VERDICT: \[TRUE\_POSITIVE\|FALSE\_POSITIVE\] REASON: \[one sentence explanation\]

Verification Prompt: Analytic DomainRole:Lean 4 and Mathlib expert specializing in real analysis formalization\.Background\.Mathlib totalizes partial functions for convenience:Real\.sqrt x = 0whenx < 0;Real\.log x = 0whenx≤\\leq0;xˆ\{\-1\} = 0whenx = 0\. A static analyzer flagged usage without the required domain guard\.Task\.Determine if the domain constraint is provable from the theorem’s hypotheses\.Domain knowledge:•ForReal\.sqrt x\(requires0≤x0\\leq x\):n2≥0n^\{2\}\\geq 0;a2\+b2\+c≥ca^\{2\}\+b^\{2\}\+c\\geq c;Nat\.castis non\-negative;\|x\|≥0\|x\|\\geq 0•ForReal\.log x\(requires0<x0<x\):1<x⇒0<x1<x\\Rightarrow 0<x;0<x∧0<y⇒0<x​y0<x\\land 0<y\\Rightarrow 0<xy;x\>0⇒xn\>0x\>0\\Rightarrow x^\{n\}\>0•Forxˆ\{\-1\}\(requiresx≠0x\\neq 0\):\[Invertible A\]impliesAAis invertible;1<x⇒x≠01<x\\Rightarrow x\\neq 0Input:\{theorem\}and\{warning\}are substituted at runtime\.Output format: VERDICT: \[TRUE\_POSITIVE\|FALSE\_POSITIVE\] REASON: \[one sentence explanation\]

Verification Prompt: Division by ZeroRole:Lean 4 and Mathlib expert specializing in formalization of arithmetic\.Background\.Division is totalized in Lean/Mathlib:x / 0 = 0by definition\. A static analyzer flagged a division without an explicit≠\\neq0guard for the divisor\.Task\.Determine if the divisor can be proven non\-zero from the theorem’s hypotheses\.Domain knowledge:•0 < ximpliesx≠\\neq0•1 < ximpliesx≠\\neq0•0 < xand0 < yimpliesx \* y≠\\neq0•Real\.sqrt x \> 0whenx \> 0•\[Fact \(p≠\\neq0\)\]typeclass provides the guard•xˆ2 \+ c \> 0whenc \> 0, so it is non\-zero•Check set/type definitions for constraints like\{p \| p\.2≠\\neq0\}Input:\{theorem\}and\{warning\}are substituted at runtime\.Output format: VERDICT: \[TRUE\_POSITIVE\|FALSE\_POSITIVE\] REASON: \[one sentence explanation\]