FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence

# FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
Source: [https://arxiv.org/html/2608.26310](https://arxiv.org/html/2608.26310)
Ziyu WangAffiliation:Academy for AdvancedAffiliation:Interdisciplinary StudiesAffiliation:Peking UniversityEmail:[wangziyu\-edu@stu\.pku\.edu\.cn](mailto:)Qiming DaiAffiliation:School of Mathematical SciencesAffiliation:Peking UniversityEmail:[qmdai25@stu\.pku\.edu\.cn](mailto:)Yishan WuAffiliation:Theory Lab, 2012 LabsAffiliation:Huawei Technologies Co\., Ltd\.Email:[wuyishan1@huawei\.com](mailto:)Zaiwen WenAffiliation:Beijing International Center forAffiliation:Mathematical ResearchAffiliation:Peking UniversityEmail:[wenzw@pku\.edu\.cn](mailto:)

###### Abstract

Large language models can now generate complex, multi\-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge\. Existing evaluation approaches largely depend on model\-based natural\-language judgments, which often overlook local reasoning gaps\. While formal theorem provers like Lean offer a path to rigorous verification, using them to evaluate informal text requires solving locality and semantic mismatches: a prover might bypass a local flaw by proving an overly broad target, or validate an auto\-formalized statement that drifts from the original mathematical intent\. To address this, we introduce FaithSieve, a Lean\-assisted framework for fine\-grained evaluation of natural\-language mathematical proofs\. FaithSieve decomposes coarse proof steps into local reasoning units, extracts typed proof obligations, and verifies them through a formal evaluation agent\. Formal validation is gated by semantic alignment scoring, so Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim\. We construct two expert\-verified datasets, ProofLoc\-Olympiad and ProofLoc\-University, to benchmark first\-error localization\. On the 350\-problem Olympiad dataset, FaithSieve using a GPT\-5\.4 backbone achieves 81\.43% exact first\-error accuracy, outperforming the direct\-judging baseline of 72\.29%\. Furthermore, on the 200\-problem ProofLoc\-University benchmark spanning six advanced domains, FaithSieve reaches 84\.5% exact accuracy, compared to 75\.0% for the direct judge\. Our work demonstrates that decomposing proofs into fine\-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural\-language reasoning\.

## 1Introduction

Large language models can now generate multi\-step mathematical proofs, but evaluating them and locating the first logical error remains difficult\. Such proofs may omit conditions, skip derivations, use implicit assumptions, or continue from early mistakes to plausible\-looking conclusions\. Reliable evaluation must therefore check not only final answers but also local reasoning steps\.

Existing natural\-language verification methods have made substantial progress\. Self\-consistency, process supervision, process reward models, and recent work on error localization, ProcessBench, Hard2Verify, and ProofGrader / ProofBench provide useful baselines for step\-level evaluation\[[Wang et al\., 2023](https://arxiv.org/html/2608.26310#bib.bib23),[Lightman et al\., 2023](https://arxiv.org/html/2608.26310#bib.bib10),[Tyen et al\., 2024](https://arxiv.org/html/2608.26310#bib.bib21),[Zheng et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib26),[Pandit et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib15),[Ma et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib11)\]\. However, their evidence mainly comes from model\-based scoring or classification over natural\-language reasoning\. In parallel, formal reasoning systems have also advanced rapidly\. Lean, mathlib, and systems such as DeepSeek\-Prover\-V2, Seed\-Prover, AxiomProver, Aria, and M2F show that many mathematical claims can now be checked with formal evidence\[[The mathlib Community, 2020](https://arxiv.org/html/2608.26310#bib.bib20),[Ren et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib17),[Chen et al\., 2025b](https://arxiv.org/html/2608.26310#bib.bib6),[Chen et al\., 2025a](https://arxiv.org/html/2608.26310#bib.bib5),[Axiom, 2026](https://arxiv.org/html/2608.26310#bib.bib2),[Wang et al\., 2025a](https://arxiv.org/html/2608.26310#bib.bib22),[Wang et al\., 2026](https://arxiv.org/html/2608.26310#bib.bib24)\]\.

Using Lean as a direct judge for informal proofs still faces a central obstacle\. Lean only verifies the formal statement submitted to it; even if that statement is provable, it need not faithfully express the proof step being checked\. Autoformalization may omit assumptions, add conditions, reverse an implication, or rewrite a contested local claim into a different statement that is provable but not equivalent\. Formal evidence is therefore useful for error localization only when the validation target remains local and semantically faithful to the original claim\.

We propose FaithSieve, a Lean\-assisted framework for first\-error localization in natural\-language mathematical proofs\. FaithSieve decomposes coarse proof steps into localEdgeUnits, extracts typed proof obligations from suspicious transitions, and combines lightweight checking, Lean validation, and semantic alignment scoring to produce local evidence\. Lean is not used as a direct judge of the whole proof; instead, it serves as a source of structured evidence gated by semantic alignment\. The overall workflow has three stages: localization, verification, and synthesis\. The localization stage constructsEdgeUnitsand selects local transitions for priority inspection\. The verification stage turns these transitions into proof obligations and gathers evidence through both formal and lightweight non\-formal checks\. The synthesis stage aggregates local evidence back to the original step level and predicts the first erroneous step\. Figure[1](https://arxiv.org/html/2608.26310#S1.F1)illustrates this pipeline\.

![Refer to caption](https://arxiv.org/html/2608.26310v1/LeanEvaluation.png)Figure 1:Overview of the FaithSieve workflow for Lean\-assisted first\-error localization\.We construct two expert\-verified datasets:ProofLoc\-Olympiad, with 350 algebra and number theory problems, andProofLoc\-University, with 200 advanced mathematics problems\. OnProofLoc\-Olympiad, FaithSieve achieves 81\.43% exact first\-error accuracy, compared with 72\.29% for a GPT\-5\.4 direct\-judging baseline\. OnProofLoc\-University, FaithSieve also obtains clear gains over direct judging\. Our contributions are as follows\.

1\.Lean\-assisted proof error localization framework\.We identify locality and semantic faithfulness as the central challenges in applying Lean validation to natural\-language proof evaluation, and propose FaithSieve as a Lean\-assisted framework for first\-error localization\. 2\.Proof\-state\-tree decomposition and typed obligations\.We introduce a proof\-state\-tree representation that decomposes coarse proof steps into local state transitions, and extract typed obligations that specify the reasoning responsibility of each transition\. 3\.Semantic alignment scoring\.We propose a semantic alignment score to measure whether a Lean statement preserves the intended informal obligation, so formal validation is used only when it avoids drifted or weakened targets\. 4\.Expert\-verified evaluation datasets\.We construct two expert\-verified benchmarks covering olympiad\-style and university\-level mathematics, and show that faithful local formal evidence improves over direct judging baselines\.

## 2Task Formulation and Challenges

### 2\.1Problem Formulation

When large language models generate natural\-language mathematical proofs, a central challenge is not only judging overall correctness but also locating the first erroneous step\. BIG\-Bench Mistake first formulated first\-mistake localization as an explicit evaluation problem, and later work extended it to mathematical process verification and open\-ended solutions\[[Tyen et al\., 2024](https://arxiv.org/html/2608.26310#bib.bib21),[Zheng et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib26),[Pandit et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib15)\]\. Process supervision and PRMs provide further background for step\-level correctness modeling\[[Lightman et al\., 2023](https://arxiv.org/html/2608.26310#bib.bib10)\]\. We adopt this formulation, but ask whether formal verification can provide checkable structured evidence for first\-error localization\.

Concretely, the input is a mathematical problemppand a natural\-language proofπ=\(s1,…,sn\)\\pi=\(s\_\{1\},\\ldots,s\_\{n\}\)withnnsteps\. The system must output eithercorrector the indexkkof the first erroneous step, wherekkrefers to a benchmark step\. We define the first erroneous step as the earliest step that makes the proof mathematically unreliable; later errors may exist, but they are not the target\.

For evaluation, we use the same label interface as prior first\-error localization work\[[Tyen et al\., 2024](https://arxiv.org/html/2608.26310#bib.bib21),[Zheng et al\., 2025](https://arxiv.org/html/2608.26310#bib.bib26)\]and report binary accuracy and exact accuracy\. Lety,y^∈\{correct\}∪\{1,…,n\}y,\\hat\{y\}\\in\\\{\\texttt\{correct\}\\\}\\cup\\\{1,\\ldots,n\\\}denote the gold label and system prediction\. Binary accuracy measures whether the system correctly distinguishes valid proofs from invalid ones, while exact accuracy requires an exact match to the gold label:correctfor valid proofs, and the correct first\-error step for invalid proofs\.

### 2\.2Lean\-Based Verification: Promise and Challenges

To go beyond purely natural\-language judges, a natural direction is to use proof assistants such as Lean to provide checkable artifacts for local mathematical claims\. Lean validation can turn part of the judgment from a model score into a verifiable proof result or failure signal\. For algebraic rewriting, logical entailment, goal reduction, witness verification, and case coverage, formal validation may provide stronger evidence than natural\-language scoring\. However, this evidence is not unconditionally reliable: formal validation must target the right local object, and that object must faithfully express the original natural\-language claim\.

Locality mismatch\.The first difficulty is ensuring that formal validation targets the same local inference as the natural\-language proof\. A proof usually consists of local reasoning transitions rather than a single theorem\. If a proof claims to derivebbfromaa, and thenccfrombb, proving onlya→ca\\to cdoes not establish that the two local stepsa→ba\\to bandb→cb\\to care correct\. A strong prover may directly prove a stronger or coarser target and ignore a local error in the original proof\. Formal validation therefore requires decomposition and localization: coarse steps must be broken into local reasoning units, and the system must choose which local claims to validate\.

Semantic mismatch\.The second difficulty is ensuring that the Lean statement faithfully represents the original obligation\. Even after localization, the system must translate the informal claim into a formal proposition\. Autoformalization may omit assumptions, add conditions, reverse implications, alter quantifiers, weaken or strengthen the conclusion, or replace the claim with a different but provable statement\. Thus, compilation or proof success alone is insufficient evidence; the key question is whether the Lean statement faithfully corresponds to the original claim\.

These two mismatches lead to two requirements\. First, formal validation should operate on local reasoning units, so the system must decompose proofs appropriately\. Second, the Lean statement being validated must be semantically aligned with the original natural\-language obligation\. Accordingly, we use Lean not as an end\-to\-end theorem prover, but as a conditional evidence generator: a formal result is strong evidence only when both locality and faithfulness are satisfied\.

## 3Localizing Verifiable Reasoning Units

### 3\.1Recursive Decomposition into a Tree of Proof States

For a traditional chain\-of\-thought proof, a COT step is suitable as an annotation and output unit, but it is often not the smallest reasoning unit, because a single step frequently contains multiple operations simultaneously: substitution, definition expansion, introduction of new facts, goal switching, or branch pruning\. If such coarse\-grained steps are passed directly to a Lean pipeline, we encounter the locality mismatch discussed in Section[2](https://arxiv.org/html/2608.26310#S2)\. Therefore, we treat a COT step as an annotation unit, but not directly as a logical verification unit\. To obtain finer\-grained proofs, we first ask the language model to pre\-decompose the original COT steps, removing redundant and repetitive statements without modifying the proof logic, and obtaining a detailed COT in a semantically faithful manner\. Here we emphasize “faithful” rather than “patching”: conclusions, variable scopes, case\-discussion wording, concrete witnesses, and numerical calculations in the original proof must all be preserved as\-is\.

A Lean proof state records the available assumptions and current goal at a given moment, and a tactic transforms one proof state into another\. Building on the fine\-grained substeps obtained from preprocessing, we borrow the state\-transition perspective of Lean proof states and ask the language model to write out all proof states and state transitions in the proof process step by step according to the natural\-language steps, constructing a tree of proof states𝒯=\(V,E\)\\mathcal\{T\}=\(V,E\)\.

Definition of a Tree of Proof States\.Each nodev∈Vv\\in Vrepresents a natural\-language proof stateSv=\(Γv,Gv\)S\_\{v\}=\(\\Gamma\_\{v\},G\_\{v\}\), whereΓv\\Gamma\_\{v\}is the currently available accumulated assumptions andGvG\_\{v\}is the current subgoal to be proved\. Taking the first step in Figure[2](https://arxiv.org/html/2608.26310#S3.F2)as an example, after the conditions and conclusion of the original problem in State 0, the natural\-language proof wishes to perform a case split on the parity ofmm\. Therefore, State 0\.0 adds the branch assumption “mmis odd” on top of the parent state and maintains the branch goal\(n,m\)=\(1,1\)\(n,m\)=\(1,1\); State 0\.1 adds the branch assumption “mmis even” and maintains the branch goal\(n,m\)=\(3,2\)\(n,m\)=\(3,2\)\. Together they correspond to the next proof states of State 0 in different proof branches\. Each edgee=\(v→v′\)∈Ee=\(v\\to v^\{\\prime\}\)\\in Erepresents a local reasoning transition of typeτe\\tau\_\{e\}, such as fact derivation, rewrite, goal reduction, case split, or lemma introduction\. Each edge is recorded as anEdgeUnitueu\_\{e\}, serving as the basic object for subsequent review and formal validation\. In the example just given, the corresponding edge type is case split\.

Figure 2:From Proof Steps to a Tree of Proof StatesRecursive construction\.In the process of constructing the proof state tree, for each pre\-decomposed substep, the model first identifies its transition typeτe\\tau\_\{e\}, then locates the parent statevvwhere this substep occurs\. For different transition types, we have written a detailed state\-transition manual to enable the LLM to accurately generate child statesSv′=\(Γv′,Gv′\)S\_\{v^\{\\prime\}\}=\(\\Gamma\_\{v^\{\\prime\}\},G\_\{v^\{\\prime\}\}\)\. For example, if the substep introduces a new facthh, we updateΓv′=Γv∪\{h\}\\Gamma\_\{v^\{\\prime\}\}=\\Gamma\_\{v\}\\cup\\\{h\\\}; if it changes the current goal, we updateGvG\_\{v\}; if it produces multiple branches, we generate multiple child nodes with branch\-specific conditions\. Edge 1 in Figure[2](https://arxiv.org/html/2608.26310#S3.F2)is a case split example: it splits State 0 into State 0\.0 and State 0\.1, corresponding tommbeing odd andmmbeing even, respectively\. We further list state\-update templates for different logical patterns in Appendix[B\.2](https://arxiv.org/html/2608.26310#A2.SS2)\. Thus, recursive construction is not merely text segmentation, but continuously maintains the local proof context carried by eachEdgeUnit\.

### 3\.2Suspicion Tree Search

After proof\-step pre\-decomposition and recursive construction of the proof\-state tree, we obtain a collection ofEdgeUnitsthat is often much larger than the original set of COT steps\. Since Lean validation is expensive, it is impractical to generate formal validation results for everyEdgeUnit\. We therefore first run Suspicion Search over all edges in the proof\-state tree, producing an initial risk tree that estimates which local transitions are more likely to contain the first material error\.

Suspicion Search uses the proof\-state information attached to eachEdgeUnit, including before\-context, after\-context, goal relation, branch scope, and transition type\. The model produces a set of one\-shot lightweight judgments: whether the transition is suspicious, how suspicious it is, and an overall suspicion risk score in\[0,1\]\[0,1\]\. During the search, we provide examples of common failure modes for different edge types and prompt the model to check for the corresponding logical errors\. Empirically, more than 80% of suspicion risk scores fall into the two extreme intervals\[0,0\.2\]\[0,0\.2\]and\[0\.8,1\.0\]\[0\.8,1\.0\]\. We therefore treat edges with suspicion risk above 0\.6 as relatively suspicious candidates\.

After scoring all edges, we build an audit window rather than selecting the globally most suspiciousEdgeUnit\. Among suspicious edges, we choose the earliest one as the focus unit and include a short prefix of preceding edges, especially those with special transition types\. This yields a cost\-controlled set of local transitions for obligation discovery and validation\.

### 3\.3Obligation Statement Generation

Table 1:Typed obligation kinds for selectedEdgeUnits\.Proof\-state tree decomposition gives us local transitions, but a transition itself is not yet a directly checkable mathematical statement\. AnEdgeUnitrecords how the proof moves from a before\-state to an after\-state: available assumptions, newly introduced conditions, goal changes, and branch or source\-step scope\. To validate such a transition, we summarize its mathematical responsibility as an explicit obligation statement\. In most cases, this statement has an implication\-like form: under the before\-context, a new claim follows; or, under the incoming context, proving the after\-goal is sufficient for proving the before\-goal\.

Concretely, we generate obligations by selecting a conversion template according to theEdgeUnit’s edge type and state change\. For common logical actions, we provide examples that map a before\-state–after\-state transition to an obligation statement, and ask the language model to instantiate the corresponding template for the current edge\. The model therefore does not freely summarize the whole proof; it generates a statement matched to the local transition under the given proof states, transition type, new conditions, and goal relation\. Table[1](https://arxiv.org/html/2608.26310#S3.T1)summarizes the main obligation kinds and their corresponding local checks\.

For example, in afact\_plus\_reductiontransition, an edge both introduces a new fact and changes the goal\. If we only check whether the after\-goal is sufficient for the before\-goal, the new claim may be used as a premise before being validated\. We therefore split this transition into two obligations: whether the new fact is supported by the prior context, and whether the goal reduction is valid when that fact is available\. For acase\_split, the obligation instead checks whether the cases are exhaustive, form a valid partition, or justify the stated branch consequence\. Thus, typed conversion turns a local edge into an explicit statement that formal validation can handle\.

## 4Faithfulness\-Aware Verification and Evidence Fusion

### 4\.1Statement Faithfulness Scoring

Given an obligationoo, letmmdenote its natural\-language statement andCCits local context\. Formal validation first generates a Lean statementm^\\hat\{m\}\. Since Lean validates onlym^\\hat\{m\}, ifm^\\hat\{m\}drops assumptions, changes objects, reverses the implication direction, or weakens the original claim, then a successful Lean proof does not establish the original obligation\. Formal validation must therefore be preceded by statement faithfulness checking\.

To measure the semantic faithfulness of the formal statementm^\\hat\{m\}to the natural\-language obligationmmunder the local contextCC, we define the statement faithfulness scoreSfaith​\(m,m^,C\)∈\[0,1\]S\_\{\\mathrm\{faith\}\}\(m,\\hat\{m\};C\)\\in\[0,1\]:

Sfaith​\(m,m^,C\)=Sprem​\(m,m^,C\)⋅Sconc​\(m,m^,C\)⋅Shol​\(m,m^,C\)\.S\_\{\\mathrm\{faith\}\}\(m,\\hat\{m\};C\)=\\sqrt\{S\_\{\\mathrm\{prem\}\}\(m,\\hat\{m\};C\)\\cdot S\_\{\\mathrm\{conc\}\}\(m,\\hat\{m\};C\)\}\\cdot S\_\{\\mathrm\{hol\}\}\(m,\\hat\{m\};C\)\.\(1\)Equation \([1](https://arxiv.org/html/2608.26310#S4.E1)\) combines premise fidelity, conclusion fidelity, and a holistic semantic score to measure whetherm^\\hat\{m\}still expresses the same local mathematical claim\. Here,SpremS\_\{\\mathrm\{prem\}\}measures whether the hypotheses ofm^\\hat\{m\}faithfully retain the local context, branch assumptions, and fixed witnesses needed by the obligation, whileSconcS\_\{\\mathrm\{conc\}\}measures whether the conclusion ofm^\\hat\{m\}matches the target claim ofmm\. LetTprem​\(m,C\)T\_\{\\mathrm\{prem\}\}\(m,C\)denote the premise\-side semantic slots extracted from the context and the source step, and letTconc​\(m\)T\_\{\\mathrm\{conc\}\}\(m\)denote the conclusion\-side semantic slots in the obligation\. The valuematch⁡\(t,m^\)∈\[0,1\]\\mathrm\{match\}\(t,\\hat\{m\}\)\\in\[0,1\]is assigned by the semantic checker rather than by string matching: for each semantic slottt, the checker compares the source slot with the hypotheses or conclusion ofm^\\hat\{m\}, and judges whether it is preserved, omitted, weakened, strengthened, or replaced\. Preserved slots receive high scores, while missing critical assumptions, altered objects, or changed claims receive low scores\. The resulting slot scores are defined in Equation \([2](https://arxiv.org/html/2608.26310#S4.E2)\)\.

Sprem=∑t∈Tpremmatch⁡\(t,m^\)\|Tprem\|​Sconc=∑t∈Tconcmatch⁡\(t,m^\)\|Tconc\|\.S\_\{\\mathrm\{prem\}\}=\\frac\{\\sum\_\{t\\in T\_\{\\mathrm\{prem\}\}\}\\mathrm\{match\}\(t,\\hat\{m\}\)\}\{\|T\_\{\\mathrm\{prem\}\}\|\}\\hskip 9\.24994ptS\_\{\\mathrm\{conc\}\}=\\frac\{\\sum\_\{t\\in T\_\{\\mathrm\{conc\}\}\}\\mathrm\{match\}\(t,\\hat\{m\}\)\}\{\|T\_\{\\mathrm\{conc\}\}\|\}\.\(2\)The holistic scoreSholS\_\{\\mathrm\{hol\}\}is determined by five aspects: step\-relation fidelity, object and witness fidelity, directionality fidelity, role\-alignment fidelity, and syntax fidelity\. It captures severe patterns beyond isolated premise or conclusion slots, including wrong direction, role reversal, meta\-level wrappers, and vacuous formalizations; details are in Appendix[C\.2](https://arxiv.org/html/2608.26310#A3.SS2)\.

Together with the faithfulness score, the semantic checker returns a structured semantic report\. This report summarizes the diagnostic information produced when the checker evaluates different aspects and semantic elements, including statement\-level status, detected drift categories, checker confidence, a natural\-language reason, missing assumptions, overgeneralization examples, and a suggested revision\. It points out the semantic differences betweenmmandm^\\hat\{m\}: which contextual assumptions are missing, which mathematical objects have been replaced, which implication direction or quantifier structure has changed, and what should be added or revised to repairm^\\hat\{m\}\.

### 4\.2Formal Evaluation Agent

Using Statement Faithfulness Scoring as a central checking tool, we develop the Formal Evaluation Agent to convert each typed obligation into local checkable evidence\. The agent runs on each obligation and returns a local evaluation result containing: \(i\) the obligation’s local checking status in\{passed,refuted,inconclusive\}\\\{\\texttt\{passed\},\\texttt\{refuted\},\\texttt\{inconclusive\}\\\}, \(ii\) evidence strength adjusted by faithfulness and checker confidence, and \(iii\) a checkable artifact or diagnostic message\. This result answers only the local obligation; it is not a proof\-level verdict\.

Formal Statement Generation\.First, the statement agent generates a local formal statementm^\\hat\{m\}or a LaTeX mathematical equation from the problem statement, theEdgeUnitsummary, and the obligation statement\. The latter is generated only when the obligation is a pure mathematical expression\. When generatingm^\\hat\{m\}, the system first asks the LLM for candidate statements and then checks whether the candidate compiles\. If it does not compile, the system invokes Lean MCP tools to repair syntax, type, or dependency errors\. After compilation succeeds, the semantic checker performs faithfulness scoring betweenm^\\hat\{m\}and the original obligationmm, returningSfaithS\_\{\\mathrm\{faith\}\}, component\-level semantic judgments, and a structured semantic report\. If the language\-meaning score or a critical component score falls below the threshold, the agent revises the statement using the drift report and repeats both compilation and semantic checking\.

Equation SymPy Checker\.We quickly handle pure numeric claims extracted in the previous step, provided they contain neither variables nor natural\-language explanation\. Concretely, the system normalizes mathematical notation from the LaTeX equation and passes the resulting expression to a SymPy\-based numeric checker\. This checker handles only pure numeric equality chains and single comparison statements, returningpassed,refuted, orinconclusive\.

Lean Prover Checker\.For other obligations whose statements pass the faithfulness gate, the agent enters the Lean validation branch\. According to the suspicion score from the audit stage, the system verifies the original proposition in Lean for obligations that are likely correct, and verifies a negated proposition or the existence of a counterexample for obligations that are likely wrong\. A proof\-search agent repeatedly interacts with the Lean MCP tools and revises the proof attempt until it succeeds or reaches the time limit\. If the original proposition is proved, the result ispassed; if the negated proposition or a counterexample is verified, the result isrefuted\. Timeout or failure to pass the faithfulness gate producesinconclusive, together with a specific inconclusive type\.

Evidence Fusion and Final Decision\.After obtaining local checking results, the system aggregates evidence back to the original COT steps\. Since oneEdgeUnitmay produce multiple obligations, fusion summarizes local review, typed obligations, formal evaluation results, faithfulness reports, and diagnostics intoInfo⁡\(ue\)\\mathrm\{Info\}\(u\_\{e\}\), then maps it to the corresponding step\. A step is markedincorrectwhen it has faithful and reliable negative evidence, such as a refuted obligation, a verified counterexample, or agreement between formal diagnostics and local review; it is markeduncertainwhen the evidence mainly reflects semantic drift, formalization failure, timeout, or conflicting diagnostics\. The system returns the earliest step with reliable negative evidence as the first error; if none is found, the LLM synthesizes all local evidence and outputscorrector a risky step\. The complete procedure is shown in Algorithm[1](https://arxiv.org/html/2608.26310#algorithm1)\.

Algorithm 1Lean\-assisted first\-error localizationInput:Problem

pp; natural\-language proof

π=\(s1,…,sn\)\\pi=\(s\_\{1\},\\ldots,s\_\{n\}\)
Output:

y^∈\{correct\}∪\{1,…,n\}\\hat\{y\}\\in\\\{\\texttt\{correct\}\\\}\\cup\\\{1,\\ldots,n\\\}
Decompose each coarse step

sis\_\{i\}into faithful fine\-grained substeps

Build state tree

𝒯=\(V,E\)\\mathcal\{T\}=\(V,E\)and normalize edges into mappedEdgeUnits

ScanEdgeUnitsand schedule audit window

WWby earliest risk and prefix coverage

foreach*scheduledEdgeUnitue∈Wu\_\{e\}\\in W*do

Run local natural\-language review and compile typed obligations

O⁡\(ue\)O\(u\_\{e\}\)
foreach*obligationo∈O⁡\(ue\)o\\in O\(u\_\{e\}\)*do

Generate a Lean statement

m^\\hat\{m\}or a LaTeX equation from

p,ue,op,u\_\{e\},o
if*oois extracted as a pure numeric claim*then

Normalize the equation and run the SymPy numeric checker

else

Compile

m^\\hat\{m\}, repairing syntax, type, or dependency errors if needed

Score faithfulness and return semantic judgments and a structured report

if*language\-meaning or critical component score is low*then

Revise

m^\\hat\{m\}using the drift report and repeat checking

if*m^\\hat\{m\}still fails the faithfulness gate or checking times out*then

Returninconclusivewith a specific type

else

Run Lean prover checker on the claim, negation, or counterexample branch

Return local result:passed,refuted, orinconclusive

Aggregate review, obligations, formal results, reports, and diagnostics into

Info⁡\(ue\)\\mathrm\{Info\}\(u\_\{e\}\)
Map

Info⁡\(ue\)\\mathrm\{Info\}\(u\_\{e\}\)back to original coarse COT steps

if*faithful reliable negative evidence is found*then

Check the preceding uncertain prefix and return the first\-error step

else

return*corrector a risky step after final LLM synthesis*

## 5Empirical Evaluation

We construct two expert\-verified datasets targeting olympiad\-style proofs and university\-level textbook proofs\. The first dataset,ProofLoc\-Olympiad, contains 350 algebra and number theory problems\. The second dataset,ProofLoc\-University, contains 200 problems across topology, linear algebra, abstract algebra, real analysis, convex analysis, and convex optimization\. Candidate proofs in both datasets are generated by GPT\-4o and then annotated by experts for proof correctness and the first erroneous coarse proof step\. Importantly, the ground\-truth label is aligned with the benchmark\-level proof step, rather than the internalEdgeUnitused by our system\.

### 5\.1Baselines and System Performance

We first evaluate the direct\-judge baseline\. This baseline provides the model with the problem statement and the original natural\-language proof, and asks it to output eithercorrector the first erroneous step in one pass\. It does not use the tree of proof states,EdgeUnits, local review, typed obligations, the Formal Evaluation Agent, or Evidence Fusion\. Thus, direct judging measures the ability of base models to localize the first error without structured decomposition or formal evidence\. Exact and binary metrics are defined in Section[2\.1](https://arxiv.org/html/2608.26310#S2.SS1)\.

The base models include GPT\-5\.4, Gemini\-3\.1\-Pro, Opus\-4\.6, DeepSeek\-v4\-Pro, GLM\-5\.1, and Qwen3\.5\-9B, covering recent frontier closed models and one 9B\-scale open\-weight model\. Model information follows the corresponding provider model cards, technical reports, or official documentation\[[OpenAI, 2026](https://arxiv.org/html/2608.26310#bib.bib13),[Google DeepMind, 2026](https://arxiv.org/html/2608.26310#bib.bib9),[Anthropic, 2026](https://arxiv.org/html/2608.26310#bib.bib1),[DeepSeek\-AI, 2026](https://arxiv.org/html/2608.26310#bib.bib7),[Zhipu AI, 2026](https://arxiv.org/html/2608.26310#bib.bib27),[Qwen Team, 2026](https://arxiv.org/html/2608.26310#bib.bib16)\]\. Table[4](https://arxiv.org/html/2608.26310#S5.T4)shows strong variation, with GPT\-5\.4 obtaining the strongest exact accuracy and Qwen3\.5\-9B serving as the 9B\-scale comparison\.

Table 2:ProofLoc\-Universitydomain distribution\.Table 3:ProofLoc\-Universitydomain results\.

Table 4:Direct\-judge base\-model results on both datasets\.The complete main\-results table is moved to Appendix[F\.4](https://arxiv.org/html/2608.26310#A6.SS4)\. It reports the performance ofFaithSieveunder different backbones and compares it with the corresponding direct\-judge setting\.FaithSievedenotes the full pipeline in Sections[3](https://arxiv.org/html/2608.26310#S3)and[4](https://arxiv.org/html/2608.26310#S4): trees of proof states andEdgeUnits, suspicion\-guided audit windows, typed obligation discovery, the Formal Evaluation Agent, statement faithfulness scoring, and Evidence Fusion\. With the GPT\-5\.4 backbone,FaithSieveachieves 81\.43% exact accuracy and 93\.71% binary accuracy onProofLoc\-Olympiad, outperforming GPT\-5\.4 direct judging at 72\.29% and 88\.29%\. OnProofLoc\-University,FaithSievereaches 84\.50% exact / 92\.50% binary accuracy, compared with 75\.00% exact / 87\.00% binary for GPT\-5\.4 direct judging\. With the Qwen3\.5\-9B backbone,FaithSieveimproves over direct judging on bothProofLoc\-OlympiadandProofLoc\-University\. Table[3](https://arxiv.org/html/2608.26310#S5.T3)further shows gains in most university domains, while Convex Optimization remains essentially tied\.

### 5\.2FaithSievePerformance and Ablations

We evaluate GPT\-5\.4 and Qwen3\.5\-9B on both datasets to test the effect of theFaithSievepipeline\. Table[5](https://arxiv.org/html/2608.26310#S5.T5)reports theProofLoc\-Olympiadresults, with experimental settings described in Appendix[F\.3](https://arxiv.org/html/2608.26310#A6.SS3); theProofLoc\-Universityresults are reported in Appendix[F\.4](https://arxiv.org/html/2608.26310#A6.SS4)\. Across both datasets and backbones,FaithSieveconsistently improves over direct judging, showing that local and faithful formal evidence benefits first\-error localization\.

We also conduct an ablation study onProofLoc\-Olympiadwith GPT\-5\.4 and Qwen3\.5\-9B to analyze which components are most important\. All ablations use a replay\-style setting, where existing intermediate artifacts are fixed and downstream components are replayed; further setup details are provided in Appendix[F\.5](https://arxiv.org/html/2608.26310#A6.SS5)\.

Table 5:Ablation results onProofLoc\-Olympiad\.The Step3 graph judge keeps decomposition and proof\-state graph artifacts, but removes local review, Lean validation, and evidence fusion\. It reaches 75\.71% exact / 88\.57% binary with GPT\-5\.4, suggesting that graph organization helps localize erroneous steps even without formal evidence\. EdgeUnit \+ NL only keeps local EdgeUnit review and final synthesis, but removes the Evaluation Agent\. It obtains 73\.43% exact / 88\.00% binary with GPT\-5\.4 and 71\.14% / 86\.00% with Qwen3\.5\-9B, showing that local EdgeUnit representations are especially helpful for the smaller backbone\.

The locality ablation removes local EdgeUnits and falls back to coarse\-step\-level judging\. GPT\-5\.4 with w/o local EdgeUnits drops to 60\.86% exact / 72\.29% binary, and Qwen3\.5\-9B with w/o local EdgeUnits obtains 62\.29% exact / 77\.71% binary\. This experiment directly supports the locality hypothesis: a benchmark step is an annotation unit, but not necessarily the actual reasoning unit\. Without decomposing coarse proof steps into local transitions, the system loses key evidence needed for first\-error localization\. The semantic\-gate ablation relaxes the translation\-confidence and statement\-confidence thresholds, allowing hybrid\-validation results to enter the final evidence set more easily\. GPT\-5\.4 with w/o semantic gate drops to 70\.86% exact / 86\.29% binary; Qwen3\.5\-9B with w/o semantic gate obtains 70\.86% exact / 86\.00% binary, also below the corresponding FullFaithSieveresult\. These results show that a Lean or checker success signal is reliable only when the statement remains semantically aligned with the original obligation; without faithfulness filtering, semantic drift contaminates the final judgment\.

## 6Conclusion

This paper studies how formal validation can serve as structured evidence for evaluating natural\-language mathematical proofs\. Our central point is simple: Lean evidence is most useful when it is local and faithful\.FaithSieveoperationalizes this view by decomposing coarse steps intoEdgeUnits, extracting typed obligations, validating selected obligations with cheap checking and Lean\-assisted agents, filtering formal evidence through semantic alignment, and fusing the result into a benchmark\-aligned first\-error prediction\. AcrossProofLoc\-OlympiadandProofLoc\-University, this local\-evidence design improves both correctness judgment and first\-error localization over direct judging, and the ablations show that local reasoning units, faithful statement checking, formal or arithmetic evidence, and evidence fusion all contribute\. More broadly,FaithSieveprovides traceable local evidence for auditing generated proofs, supporting step\-level feedback, and exposing where a proof first becomes unreliable; future work should extend this approach to geometry, combinatorics, and definition\-heavy university mathematics while improving autoformalization and validation efficiency\.

## References

- Anthropic \[2026\]Anthropic\.Claude Opus 4\.6 model documentation, 2026\.Provider model documentation\.
- Axiom \[2026\]Axiom\.AXLE documentation, 2026\.URL[https://axle\.axiommath\.ai/v1/docs/](https://axle.axiommath.ai/v1/docs/)\.Accessed: 2026\-05\-02\.
- Axler \[2015\]Sheldon Axler\.*Linear Algebra Done Right*\.Springer, 3 edition, 2015\.
- Boyd and Vandenberghe \[2004\]Stephen Boyd and Lieven Vandenberghe\.*Convex Optimization*\.Cambridge University Press, 2004\.
- Chen et al\. \[2025a\]Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, and Thomas Hanwen Zhu\.Seed\-prover 1\.5: Mastering undergraduate\-level theorem proving via learning from experience\.*arXiv preprint arXiv:2512\.17260*, 2025a\.doi:10\.48550/arXiv\.2512\.17260\.URL[https://arxiv\.org/abs/2512\.17260](https://arxiv.org/abs/2512.17260)\.
- Chen et al\. \[2025b\]Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu\.Seed\-prover: Deep and broad reasoning for automated theorem proving\.*arXiv preprint arXiv:2507\.23726*, 2025b\.doi:10\.48550/arXiv\.2507\.23726\.URL[https://arxiv\.org/abs/2507\.23726](https://arxiv.org/abs/2507.23726)\.
- DeepSeek\-AI \[2026\]DeepSeek\-AI\.DeepSeek\-v4\-Pro technical report or model documentation, 2026\.Provider model documentation\.
- Dummit and Foote \[2004\]David S\. Dummit and Richard M\. Foote\.*Abstract Algebra*\.John Wiley & Sons, 3 edition, 2004\.
- Google DeepMind \[2026\]Google DeepMind\.Gemini 3\.1 Pro model documentation, 2026\.Provider model documentation\.
- Lightman et al\. \[2023\]Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe\.Let’s verify step by step\.*arXiv preprint arXiv:2305\.20050*, 2023\.doi:10\.48550/arXiv\.2305\.20050\.URL[https://arxiv\.org/abs/2305\.20050](https://arxiv.org/abs/2305.20050)\.
- Ma et al\. \[2025\]Wenjie Ma, Andrei Cojocaru, Neel Kolhe, Bradley Louie, Robin Said Sharif, Haihan Zhang, Vincent Zhuang, Matei Zaharia, and Sewon Min\.Reliable fine\-grained evaluation of natural language math proofs\.*arXiv preprint arXiv:2510\.13888*, 2025\.doi:10\.48550/arXiv\.2510\.13888\.URL[https://arxiv\.org/abs/2510\.13888](https://arxiv.org/abs/2510.13888)\.
- Munkres \[2000\]James R\. Munkres\.*Topology*\.Prentice Hall, 2 edition, 2000\.
- OpenAI \[2026\]OpenAI\.GPT\-5\.4 model documentation, 2026\.Provider model documentation\.
- OptSuite \[2026\]OptSuite\.Lean tools MCP: A lean 4 MCP server for proof\-assistant workflows\.[https://github\.com/optsuite/lean\-tools\-mcp](https://github.com/optsuite/lean-tools-mcp), 2026\.Accessed: 2026\-05\-07\.
- Pandit et al\. \[2025\]Shrey Pandit, Austin Xu, Xuan\-Phi Nguyen, Yifei Ming, Caiming Xiong, and Shafiq Joty\.Hard2verify: A step\-level verification benchmark for open\-ended frontier math\.*arXiv preprint arXiv:2510\.13744*, 2025\.doi:10\.48550/arXiv\.2510\.13744\.URL[https://arxiv\.org/abs/2510\.13744](https://arxiv.org/abs/2510.13744)\.
- Qwen Team \[2026\]Qwen Team\.Qwen3\.5\-9B technical report or model documentation, 2026\.Provider model documentation\.
- Ren et al\. \[2025\]Z\. Z\. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z\. F\. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan\.Deepseek\-prover\-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.*arXiv preprint arXiv:2504\.21801*, 2025\.doi:10\.48550/arXiv\.2504\.21801\.URL[https://arxiv\.org/abs/2504\.21801](https://arxiv.org/abs/2504.21801)\.
- Rockafellar \[1970\]R\. Tyrrell Rockafellar\.*Convex Analysis*\.Princeton University Press, 1970\.
- Tao \[2016\]Terence Tao\.*Analysis II*\.Hindustan Book Agency, 3 edition, 2016\.
- The mathlib Community \[2020\]The mathlib Community\.The lean mathematical library\.In*Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs*, pages 367–381\. Association for Computing Machinery, 2020\.doi:10\.1145/3372885\.3373824\.URL[https://dl\.acm\.org/doi/10\.1145/3372885\.3373824](https://dl.acm.org/doi/10.1145/3372885.3373824)\.
- Tyen et al\. \[2024\]Gladys Tyen, Hassan Mansoor, Victor Carbune, Peter Chen, and Tony Mak\.LLMs cannot find reasoning errors, but can correct them given the error location\.In*Findings of the Association for Computational Linguistics: ACL 2024*, pages 13894–13908, Bangkok, Thailand, 2024\. Association for Computational Linguistics\.doi:10\.18653/v1/2024\.findings\-acl\.826\.URL[https://aclanthology\.org/2024\.findings\-acl\.826/](https://aclanthology.org/2024.findings-acl.826/)\.
- Wang et al\. \[2025a\]Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, and Bin Dong\.Aria: An agent for retrieval and iterative auto\-formalization via dependency graph\.*arXiv preprint arXiv:2510\.04520*, 2025a\.doi:10\.48550/arXiv\.2510\.04520\.URL[https://arxiv\.org/abs/2510\.04520](https://arxiv.org/abs/2510.04520)\.
- Wang et al\. \[2023\]Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou\.Self\-consistency improves chain of thought reasoning in language models\.In*International Conference on Learning Representations*, 2023\.doi:10\.48550/arXiv\.2203\.11171\.URL[https://arxiv\.org/abs/2203\.11171](https://arxiv.org/abs/2203.11171)\.
- Wang et al\. \[2026\]Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, and Zaiwen Wen\.M2F: Automated formalization of mathematical literature at scale\.*arXiv preprint arXiv:2602\.17016*, 2026\.doi:10\.48550/arXiv\.2602\.17016\.URL[https://arxiv\.org/abs/2602\.17016](https://arxiv.org/abs/2602.17016)\.
- Wang et al\. \[2025b\]Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang, Shihao Zhou, Bin Dong, and Zaiwen Wen\.Translating informal proofs into formal proofs using a chain of states\.*arXiv preprint arXiv:2512\.10317*, 2025b\.URL[https://arxiv\.org/abs/2512\.10317](https://arxiv.org/abs/2512.10317)\.
- Zheng et al\. \[2025\]Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin\.Processbench: Identifying process errors in mathematical reasoning\.In*Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics*, 2025\.doi:10\.48550/arXiv\.2412\.06559\.URL[https://arxiv\.org/abs/2412\.06559](https://arxiv.org/abs/2412.06559)\.arXiv:2412\.06559\.
- Zhipu AI \[2026\]Zhipu AI\.GLM\-5\.1 model documentation, 2026\.Provider model documentation\.

###### Appendix Contents

1. [1Introduction](https://arxiv.org/html/2608.26310#S1)
2. [2Task Formulation and Challenges](https://arxiv.org/html/2608.26310#S2)1. [2\.1Problem Formulation](https://arxiv.org/html/2608.26310#S2.SS1) 2. [2\.2Lean\-Based Verification: Promise and Challenges](https://arxiv.org/html/2608.26310#S2.SS2)
3. [3Localizing Verifiable Reasoning Units](https://arxiv.org/html/2608.26310#S3)1. [3\.1Recursive Decomposition into a Tree of Proof States](https://arxiv.org/html/2608.26310#S3.SS1) 2. [3\.2Suspicion Tree Search](https://arxiv.org/html/2608.26310#S3.SS2) 3. [3\.3Obligation Statement Generation](https://arxiv.org/html/2608.26310#S3.SS3)
4. [4Faithfulness\-Aware Verification and Evidence Fusion](https://arxiv.org/html/2608.26310#S4)1. [4\.1Statement Faithfulness Scoring](https://arxiv.org/html/2608.26310#S4.SS1) 2. [4\.2Formal Evaluation Agent](https://arxiv.org/html/2608.26310#S4.SS2)
5. [5Empirical Evaluation](https://arxiv.org/html/2608.26310#S5)1. [5\.1Baselines and System Performance](https://arxiv.org/html/2608.26310#S5.SS1) 2. [5\.2FaithSievePerformance and Ablations](https://arxiv.org/html/2608.26310#S5.SS2)
6. [6Conclusion](https://arxiv.org/html/2608.26310#S6)
7. [References](https://arxiv.org/html/2608.26310#bib)
8. [AIntroduction to Lean and Mathlib](https://arxiv.org/html/2608.26310#A1)
9. [BLocal Reasoning Unit Construction](https://arxiv.org/html/2608.26310#A2)1. [B\.1Faithful Proof Decomposition Prompt](https://arxiv.org/html/2608.26310#A2.SS1) 2. [B\.2Tree of Proof State](https://arxiv.org/html/2608.26310#A2.SS2) 3. [B\.3Tree\-Suspicion Scan and Local Review](https://arxiv.org/html/2608.26310#A2.SS3) 4. [B\.4Typed Obligation Discovery](https://arxiv.org/html/2608.26310#A2.SS4)
10. [CFormal Evaluation Agent](https://arxiv.org/html/2608.26310#A3)1. [C\.1Cheap Arithmetic Checker](https://arxiv.org/html/2608.26310#A3.SS1) 2. [C\.2Statement Semantic Checker](https://arxiv.org/html/2608.26310#A3.SS2) 3. [C\.3Statement / Proof Generation and Compile Repair](https://arxiv.org/html/2608.26310#A3.SS3)
11. [DProofLoc Dataset](https://arxiv.org/html/2608.26310#A4)1. [D\.1Dataset Summary and Source Provenance](https://arxiv.org/html/2608.26310#A4.SS1) 2. [D\.2Data Generation](https://arxiv.org/html/2608.26310#A4.SS2)
12. [EHuman Audits of Pipeline Components](https://arxiv.org/html/2608.26310#A5)1. [E\.1Human Audits of Local Reasoning Construction](https://arxiv.org/html/2608.26310#A5.SS1) 2. [E\.2Human Calibration of the Semantic Gate](https://arxiv.org/html/2608.26310#A5.SS2)
13. [FAdditional Experimental Details and Ablations](https://arxiv.org/html/2608.26310#A6)1. [F\.1Tree Scale and Scheduling Sparsity](https://arxiv.org/html/2608.26310#A6.SS1) 2. [F\.2Direct Judge Baseline](https://arxiv.org/html/2608.26310#A6.SS2) 3. [F\.3FaithSieve Pipeline Settings](https://arxiv.org/html/2608.26310#A6.SS3) 4. [F\.4Full Main Results](https://arxiv.org/html/2608.26310#A6.SS4) 5. [F\.5Ablation Study and Analysis](https://arxiv.org/html/2608.26310#A6.SS5) 6. [F\.6Label Balance and End\-to\-End Error Decomposition](https://arxiv.org/html/2608.26310#A6.SS6) 7. [F\.7Multi\-Sample, Deliberative, and External Baselines](https://arxiv.org/html/2608.26310#A6.SS7) 8. [F\.8Token Cost and High\-Budget Controls](https://arxiv.org/html/2608.26310#A6.SS8) 9. [F\.9Domain\-Level Uncertainty](https://arxiv.org/html/2608.26310#A6.SS9) 10. [F\.10Decoding Configuration of the Original University Experiment](https://arxiv.org/html/2608.26310#A6.SS10)
14. [GLimitations and Broader Impacts](https://arxiv.org/html/2608.26310#A7)1. [G\.1Limitations](https://arxiv.org/html/2608.26310#A7.SS1) 2. [G\.2Broader Impacts](https://arxiv.org/html/2608.26310#A7.SS2)
15. [HCase Studies: Natural\-Language Context for Representative Lean Statements](https://arxiv.org/html/2608.26310#A8)

## Appendix AIntroduction to Lean and Mathlib

Lean is a dependent\-type\-theoretic interactive theorem prover\. A mathematical theorem is first stated as a formal proposition, and a proof is accepted only when Lean’s kernel verifies that the submitted proof object has the required type\. In practice, proofs are often written in tactic mode: instead of constructing the entire proof term at once, the user applies a sequence of tactics that incrementally transform the current proof situation until no obligation remains\.

Mathlib is Lean’s community\-maintained mathematical library\. It provides a large body of definitions, lemmas, theorem statements, notation, tactics, and domain\-specific infrastructure\. For the purposes of this paper, mathlib largely determines the practical boundary of Lean validation: a natural\-language obligation is easier to formalize and check when its objects and background facts can be expressed using existing mathlib definitions and lemmas\. Accordingly, Lean evidence in our framework is not merely a consequence of the Lean kernel; it also depends on whether the generated statement faithfully represents the original claim and whether the relevant mathematical vocabulary is available in Lean/mathlib\[[The mathlib Community, 2020](https://arxiv.org/html/2608.26310#bib.bib20)\]\.

Following the state\-and\-tactic view developed in prior work on Chain of States for Lean formalization\[[Wang et al\., 2025b](https://arxiv.org/html/2608.26310#bib.bib25)\], a proof state in Lean represents the complete local proof environment at a particular moment\. Formally, a state can be viewed as a finite collection of goals,

S=\{G1,…,Gn\},S=\\\{G\_\{1\},\\ldots,G\_\{n\}\\\},where each goal has the form

\{h1,…,hm\}⊢g\.\\\{h\_\{1\},\\ldots,h\_\{m\}\\\}\\vdash g\.Here\{h1,…,hm\}\\\{h\_\{1\},\\ldots,h\_\{m\}\\\}is the local hypothesis context of that goal, andggis the target conclusion that remains to be proved\. This is why a proof state captures the full local context of the proof at a given moment: it records not only the theorem being pursued, but also all currently open subgoals, their local assumptions, introduced variables, branch hypotheses, intermediate facts, and remaining targets\.

A tactic is an operation that transforms one proof state into another\. Applying a tactic may solve a goal, replace it with simpler subgoals, split it into cases, introduce variables or assumptions, rewrite the target, add derived facts to the context, or invoke an existing lemma from mathlib\. A tactic proof can therefore be written as a sequence

S0→T1S1→T2⋯→TkSk\.S\_\{0\}\\xrightarrow\{T\_\{1\}\}S\_\{1\}\\xrightarrow\{T\_\{2\}\}\\cdots\\xrightarrow\{T\_\{k\}\}S\_\{k\}\.The proof is complete if and only if the final state has no remaining goals\. During this process, the number and shape of goals can change substantially: a single goal may split into several branch goals after a case analysis; a difficult target may be reduced to auxiliary lemma subgoals; and solved branches disappear from the state\.

This paper’s notion ofProof State Changeis inspired by this Lean mechanism, but is used at the level of natural\-language proof evaluation\. We do not assume that every natural\-language step has already been formalized as an executable Lean tactic\. Instead, we represent a local reasoning transition as a change from a before\-state to an after\-state\. The before\-state records the assumptions, facts, branch conditions, and current goal available before the step; the after\-state records what the step claims to add, transform, reduce, split, or discharge\. A valid local proof step should therefore correspond to a faithful and justified proof\-state change: newly introduced facts must follow from the previous context, rewritten expressions must preserve meaning, case splits must cover the original goal, witnesses must satisfy their required properties, and goal reductions must be logically equivalent to, or sufficient for, the original target\.

This perspective is central toFaithSieve\. Rather than asking Lean or an LLM to judge an entire natural\-language proof globally, we decompose the proof into local transitions between proof states\. Each transition can then be converted into typed obligations and, when appropriate, checked using Lean/mathlib evidence\. Lean proof success is useful only when the generated Lean statement faithfully represents the intended proof\-state change; proof failure or timeout is treated as inconclusive rather than as direct evidence that the original proof is wrong\.

## Appendix BLocal Reasoning Unit Construction

This section describes the local proof\-structure construction used in Section[3](https://arxiv.org/html/2608.26310#S3)\. The pipeline first decomposes a coarse natural\-language proof into faithful fine\-grained steps, then builds a natural\-language proof\-state tree, normalizes each tree edge as anEdgeUnit, and finally converts selected units into typed obligations\. Decomposition, tree construction, tree suspicion scan, and local review are prompt\-driven\. Typed obligation discovery is governed by deterministic transition typing and obligation\-generation rules; the prompts and algorithmic rules are included below for reproducibility\.

### B\.1Faithful Proof Decomposition Prompt

The decomposition prompt asks the model to split each original proof step into fine\-grained substeps while preserving the mathematical content of the original proof\. The model is instructed not to repair incorrect equations, missing hypotheses, invalid witnesses, branch assumptions, concrete numerical values, or over\-strong conclusions\. The stage also keeps pointers from fine\-grained steps back to the original coarse step\.

Prompt for Faithful Proof Decomposition

Foreachoriginalproofstep,splititintofine\-grainedsubsteps\.

Rules:

1\.Eachsubstepshouldcontainexactlyonelogicalinferencewheneverpossible\.

2\.Donotcorrectmathematicalerrors\.

3\.Preserveallequations,inequalities,constants,witnesses,variablescopes,

andbranchassumptions\.

4\.Preservedecisivewordssuchasonly,all,exists,unique,least,greatest,

must,valid,andsufficient\.

5\.Removeonlymotivation\-onlyorrestatement\-onlysentencesthatintroduceno

newreasoning\.

6\.Ifastepcontainsasubstitution,arewrite,anewfact,andagoalchange,

splitthemintoseparatesubsteps\.

7\.Ifasubstepisinsideacase,contradiction,induction,orwitnessscope,

statethatscopeexplicitly\.

Output:

Foreachoriginalstepi,returnsubstepsi\.1,i\.2,…andkeepapointerto

theoriginalstep\.

A repair\-prevention check flags strengthening, weakening, dropped decisive words, changed constants, missing branch scope, and action\-result splits that make the original inference look more justified than it was\.

### B\.2Tree of Proof State

The tree of proof states is a natural\-language structure inspired by Lean proof states\. Each state records accumulated assumptions and a current local goal, while each edge records a reasoning transition\. A state describes what is available after a step, not what the step itself says\. Goals normally remain the final target except in lemma, witness, induction, or iff subtrees\.

Prompt for Tree of Informal Proof State

InformalProofStatefromadetailedChainofThought\(CoT\)\.

\-EachstatecontainsConditionsandaGoal\.

\-ConditionsareALLhypotheses/factsavailableatthispoint\.

\-TheGoalistheFINALtargettoprove,nottheintermediatestep’sconclusion\.

\-AStaterepresentstheaccumulatedproofcontextAFTERareasoningstepis

applied,NOTthestepitself\.

Conditionaccumulation:

1\.Eachchildstateinheritsallconditionsfromitsparent,plusanynew

conditionsderivedinthatstep\.

2\.Giveeachconditionashortname\.

3\.Somestepstransformconditions,suchasexistentialelimination,

disjunctionelimination,andhave/lemmaintroduction\.

One\-to\-onemapping:

EVERYCoTStepMUSTcorrespondtoEXACTLYONEedgeinthetree\.

Donotskip,merge,orinventCoT\-stepedges\.

Foreachedge,provideStepExplanationmetadata:

Pattern,GoalRelation,RetainedConditions,NewConditions,

Removed/ConsumedConditions,TransformedConditions,andExplanation\.

Every parsed tree edge is normalized as anEdgeUnit\. The structure stores identity fieldsunit\_id,edge\_index,parent, andchildren; provenance fieldsdetailed\_step\_idx,original\_step\_idx, andoriginal\_step\_text; transition metadatapattern,explanation, andgoal\_relation; before/after goals and conditions; delta fields such asnew\_conditionsandnew\_condition\_details; structural cues such as branch scope and consumed or transformed conditions; and scheduling hints such asis\_signature,signature\_reasons, and local risk flags\.

In representative Olympiad\-style generated examples, a GPT\-5\.4EdgeUnitfor the step “By closure under addition, their sumu\+wu\+wmust lie inU∪WU\\cup W” records the new conditionh\_sum\_in\_union:u\+w∈U∪Wu\+w\\in U\\cup Wwhile keeping the overall iff goal\. A Qwen3\.5\-9B OlympiadBench example for a complex\-number inequality problem produces a noisier same\-goal unit whose new condition is a partial answer\-path statement about expressing\|z1−z2\|\|z\_\{1\}\-z\_\{2\}\|in terms ofKKand solving for the smallest positive integerKK\. Both examples are informative: clean units expose local mathematical deltas, while malformed units expose structure that downstream review should inspect rather than silently smooth away\.

### B\.3Tree\-Suspicion Scan and Local Review

The tree scan ranks suspicious units and marks which ones are worth local review or formalization\. It is not a final proof verdict\. In the experiments, the audit window size is fixed to 6: for a suspicious fine\-grained step, the window contains that step together with up to six preceding fine\-grained steps\. This prefix window is designed for first\-error localization, since an error may become salient only after later reasoning has propagated it\.

System Prompt for Tree\-Suspicion Scan

Youaregivenaprooftreealreadybuiltfromaproof\.YourjobisNOTto

formalizeanything\.

Yourjobisonlytorankwhichedges/segmentsaremostsuspicious,withspecial

emphasisontheearliestplausibleerror\.

ReturncompactJSONonly\.

User Prompt Template for Tree\-Suspicion Scan

\{problem\_statement\}

Originalproof:

\{original\_proof\}

Proof\-treeunits:

\{renderedEdgeUnitsummaries\}

ReturnJSONwithschema:

\{

"overall\_verdict":"likely\_correct"\|"likely\_incorrect"\|"uncertain",

"candidates":\[

\{

"unit\_id":"edge\_0",

"suspicion":0\.0,

"likely\_wrong":true,

"should\_formalize":true,

"error\_type\_prior":\["arithmetic"\],

"reason":"…"

\}

\]

\}

Rules:

\-Focusontheearliestplausibleerror\.

\-Suspicionmustbebetween0and1\.

\-Markshould\_formalize=trueonlyforunitswhereformalorprecisechecking

looksuseful\.

\-Ifunsure,stillprovideacandidatelistwithlow\-to\-mediumsuspicionvalues\.

For scheduled units, the local reviewer consumes one unit plus the tree\-scan prior and returns a JSON verdict, suspicion score, error type, formalization flag, translation difficulty, and reason\.

### B\.4Typed Obligation Discovery

Typed obligation discovery converts a selected local transition into explicit natural\-language verification targets\. The key rule is that newly introduced facts cannot be used as premises before those facts have themselves been checked\.

Rule Prompt for Typed Obligation Discovery

\-EdgeUnituwithbefore\-state\(Gamma\_in\|\-G\_in\),after\-state\(Gamma\_out\|\-G\_out\),

transitionmetadata,newconditions,andsourceprooftext\.

\-Localreviewrwithverdict,suspicion,errortype,should\_formalize,and

translation\_difficulty\.

Step1:Infertransitiontype\.

\-Iftextmentionscase/split:case\_split\.

\-Iftextintroduceswitness/choose/take/let/define:witness\.

\-Ifgoalchangesandnewconditionsexist:fact\_plus\_reduction\.

\-Ifgoalchangeswithoutnewconditions:goal\_reduction\.

\-Iftextsuggestsrewrite/simplify/factor/expand/substitute/evaluate/arithmetic:

rewrite\.

\-Otherwise:derived\_fact\.

Step2:Generateobligationbundle\.

\-derived\_fact/rewrite:createobligationsforthenewlyintroducedclaims\.

\-goal\_reduction:checkthatG\_outissufficienttoproveG\_in\.

\-fact\_plus\_reduction:checkthenewfactfirst,thencheckthereduction\.

\-witness:checktheintroducedwitnessorobject\.

\-case\_split:choosecase\_split,branch\_elimination,

justification\_faithfulness,oroverlap\_partition\.

Outputfields:

obligation\_id,unit\_id,kind,statement,reason,use\_lean,

translation\_confidence,source,lean\_priority\.

The obligation kinds includederived\_fact,rewrite,goal\_reduction,fact\_plus\_reduction,contested\_claim,entailment,case\_split,branch\_elimination,justification\_faithfulness,overlap\_partition, andwitness\. These obligations are still natural\-language verification targets; Appendix[C](https://arxiv.org/html/2608.26310#A3)describes how they are checked by cheap arithmetic routines, Lean validation, semantic alignment, and evidence fusion\.

## Appendix CFormal Evaluation Agent

This section expands the Formal Evaluation Agent described in Section[4](https://arxiv.org/html/2608.26310#S4)\. The agent evaluates one typed local obligation at a time and returns local evidence, not a global proof verdict\. Its result is one ofpassed,refuted, orinconclusive, together with a faithfulness score, Lean artifact, diagnostic trace, or semantic\-drift report\.

### C\.1Cheap Arithmetic Checker

The cheap arithmetic checker is a deliberately narrow front\-end filter for obligations that are pure numerical claims\. It handles numeric equalities, equality chains, and single numeric comparisons\. Examples include3\+4=73\+4=7,1\+2=3=91\+2=3=\\sqrt\{9\}, and5<85<8\. The checker is used only when the extracted claim contains no variables, functions, quantifiers, ellipses, branch conditions, named mathematical objects, or natural\-language predicates\. This conservative scope is important: the checker is meant to catch obvious arithmetic mistakes at low cost, not to decide symbolic algebraic claims or obligations whose meaning depends on context\.

Operationally, the agent normalizes the mathematical surface form into a restricted expression grammar\. It accepts numerals, rational constants, decimal constants, parentheses, arithmetic operators, exponentiation with numeric exponent, standard comparisons, and equality\-chain separators\. LaTeX tokens such as\\frac\{a\}\{b\},\\sqrt\{a\},\\cdot, and comparison symbols are normalized before evaluation\. The parsed expression is evaluated exactly when possible using rational arithmetic; otherwise the checker falls back to high\-precision numeric evaluation with a strict tolerance policy\. Equality chains are checked pairwise from left to right\. A claim is returned aspassedonly if all comparisons are verified,refutedif a pure numeric comparison is false, andinconclusiveif parsing fails or if the claim falls outside the accepted grammar\.

### C\.2Statement Semantic Checker

The statement semantic checker implements the faithfulness gate in Section[4](https://arxiv.org/html/2608.26310#S4)\. Given a natural\-language obligationmm, its local contextCC, and a generated Lean statementm^\\hat\{m\}, the checker asks whetherm^\\hat\{m\}expresses the same local mathematical claim asmm\. It does not decide whether the claim is true and does not inspect whether a Lean proof succeeds\. Its role is to prevent a provable but semantically shifted Lean theorem from being treated as evidence for the original obligation\.

#### Semantic slots andmatch⁡\(t,t′\)\\mathrm\{match\}\(t,t^\{\\prime\}\)\.

The checker first extracts semantic slots from the source obligation and context\. Premise\-side slotsTprem​\(m,C\)T\_\{\\mathrm\{prem\}\}\(m,C\)include local assumptions, branch hypotheses, declared domains, fixed variables, nonzero or positivity conditions, and witnesses that the obligation is allowed to use\. Conclusion\-side slotsTconc​\(m\)T\_\{\\mathrm\{conc\}\}\(m\)include the claimed equality, inequality, implication, set relation, existence claim, uniqueness claim, goal reduction, or branch\-coverage target\.

The generated Lean statementm^\\hat\{m\}is also rendered into a structured semantic view\. LetT⁡\(m^\)T\(\\hat\{m\}\)be the slots extracted fromm^\\hat\{m\}, partitioned into Lean premise slots and Lean conclusion slots\. For each source slottt, the checker selects the best corresponding Lean slot

t⋆​\(t,m^\)=arg⁡maxt′∈T⁡\(m^\)⁡match⁡\(t,t′\),t^\{\\star\}\(t,\\hat\{m\}\)=\\arg\\max\_\{t^\{\\prime\}\\in T\(\\hat\{m\}\)\}\\mathrm\{match\}\(t,t^\{\\prime\}\),where the candidate set is restricted to premise slots whent∈Tpremt\\in T\_\{\\mathrm\{prem\}\}and to conclusion slots whent∈Tconct\\in T\_\{\\mathrm\{conc\}\}, except that the checker may explicitly flag a role swap if a source premise appears only as a Lean conclusion or vice versa\.

The slot\-level scorematch⁡\(t,t′\)∈\[0,1\]\\mathrm\{match\}\(t,t^\{\\prime\}\)\\in\[0,1\]is assigned by the following rubric:

When no suitable Lean slot exists,match⁡\(t,⊥\)=0\\mathrm\{match\}\(t,\\bot\)=0\. If a slot is strengthened or weakened, the score depends on whether the change affects the evidential use of the Lean result\. For example, adding an extra assumption to a Lean theorem can make the statement easier and therefore less faithful, while dropping a positivity condition can make an originally valid local inference invalid\.

The premise and conclusion scores are

Sprem​\(m,m^,C\)=1\|Tprem​\(m,C\)\|​∑t∈Tprem​\(m,C\)maxt′∈Tprem​\(m^\)⁡match⁡\(t,t′\),S\_\{\\mathrm\{prem\}\}\(m,\\hat\{m\};C\)=\\frac\{1\}\{\|T\_\{\\mathrm\{prem\}\}\(m,C\)\|\}\\sum\_\{t\\in T\_\{\\mathrm\{prem\}\}\(m,C\)\}\\max\_\{t^\{\\prime\}\\in T\_\{\\mathrm\{prem\}\}\(\\hat\{m\}\)\}\\mathrm\{match\}\(t,t^\{\\prime\}\),Sconc​\(m,m^,C\)=1\|Tconc​\(m\)\|​∑t∈Tconc​\(m\)maxt′∈Tconc​\(m^\)⁡match⁡\(t,t′\)\.S\_\{\\mathrm\{conc\}\}\(m,\\hat\{m\};C\)=\\frac\{1\}\{\|T\_\{\\mathrm\{conc\}\}\(m\)\|\}\\sum\_\{t\\in T\_\{\\mathrm\{conc\}\}\(m\)\}\\max\_\{t^\{\\prime\}\\in T\_\{\\mathrm\{conc\}\}\(\\hat\{m\}\)\}\\mathrm\{match\}\(t,t^\{\\prime\}\)\.If a slot set is empty because the obligation has no explicit premises or no explicit conclusion\-side modifiers, the corresponding average is defined over a singleton vacuous slot with score 1, unless the checker detects that the formal statement introduced unsupported structure\. The final faithfulness score is the one used in Section[4](https://arxiv.org/html/2608.26310#S4):

Sfaith​\(m,m^,C\)=Sprem​\(m,m^,C\)⋅Sconc​\(m,m^,C\)⋅Shol​\(m,m^,C\)\.S\_\{\\mathrm\{faith\}\}\(m,\\hat\{m\};C\)=\\sqrt\{S\_\{\\mathrm\{prem\}\}\(m,\\hat\{m\};C\)\\cdot S\_\{\\mathrm\{conc\}\}\(m,\\hat\{m\};C\)\}\\cdot S\_\{\\mathrm\{hol\}\}\(m,\\hat\{m\};C\)\.

#### Five\-aspect holistic scoring prompt\.

The holistic scoreSholS\_\{\\mathrm\{hol\}\}is produced by a five\-aspect semantic scoring prompt\. Each aspect is scored in\{0,0\.25,0\.5,0\.75,1\}\\\{0,0\.25,0\.5,0\.75,1\\\}, and the final holistic value is

Shol=0\.20​Sstep\+0\.20​Sobj\+0\.20​Sdir\+0\.20​Srole\+0\.20​Ssyn\.S\_\{\\mathrm\{hol\}\}=0\.20S\_\{\\mathrm\{step\}\}\+0\.20S\_\{\\mathrm\{obj\}\}\+0\.20S\_\{\\mathrm\{dir\}\}\+0\.20S\_\{\\mathrm\{role\}\}\+0\.20S\_\{\\mathrm\{syn\}\}\.The uniform weighting treats the five holistic aspects as equally necessary safeguards: even if the same mathematical expression appears, the statement is not faithful if it certifies the wrong transition, changes objects, reverses direction, swaps logical roles, or collapses into a vacuous surface form\.

Prompt for Statement Semantic Checking

YouareastrictsemanticcheckerforLeanautoformalization\.

Yourtaskisnottoprovethestatement\.Yourtaskistojudgewhetherthe

Leanstatementfaithfullyrepresentsthenatural\-languagelocalobligation

underthegivencontext\.

Input:

1\.Problemstatement\.

2\.SourceproofstepandlocalEdgeUnitcontext\.

3\.Natural\-languageobligationm\.

4\.GeneratedLeanstatementm\_hat\.

5\.OptionalLeandiagnosticsfromcompilation\.

Scoreeachaspectusingonly\{0,0\.25,0\.5,0\.75,1\}\.

AspectA:step\_relation\_fidelity\.

Doesm\_hatformalizethesamelocalproof\-statetransitionasm?

Checkwhetheritvalidatesthesamenewlyintroducedfact,rewrite,

goalreduction,witnesscheck,casesplit,orbranchelimination\.

AspectB:object\_witness\_fidelity\.

Arethemathematicalobjects,domains,constants,functions,sets,

indices,witnesses,andbranch\-specificvariablesthesame?

AspectC:directionality\_fidelity\.

Areimplicationdirection,iffdirection,equalityorientation,

goal\-reductiondirection,quantifierorder,andnegationpolaritypreserved?

AspectD:role\_alignment\_fidelity\.

Areassumptions,conclusions,definitions,intermediateclaims,andgoals

keptinthesamelogicalroles?

AspectE:syntax\_surface\_fidelity\.

Istheformalstatementadirectmathematicalstatementratherthana

vacuouswrapper,placeholder,trivialtheorem,malformedparse,or

meta\-levelassertion?

ReturncompactJSON:

\{

"scores":\{

"step\_relation\_fidelity":0\.0,

"object\_witness\_fidelity":0\.0,

"directionality\_fidelity":0\.0,

"role\_alignment\_fidelity":0\.0,

"syntax\_surface\_fidelity":0\.0

\},

"holistic\_score":0\.0,

"status":"faithful"\|"repairable\_drift"\|"unfaithful",

"drift\_categories":\[

"missing\_assumptions",

"overgeneralized",

"undergeneralized",

"wrong\_objects",

"wrong\_quantifiers",

"wrong\_direction",

"role\_swap",

"vacuous\_or\_trivialized"

\],

"reason":"…",

"missing\_or\_changed\_slots":\["…"\],

"suggested\_revision":"…"

\}

The checker returnsfaithfulonly when the total faithfulness score and all critical component scores exceed the threshold\. Directionality, role alignment, and conclusion fidelity are treated as critical: a high average score cannot compensate for proving the converse, assuming the target, or changing the contested conclusion\.

### C\.3Statement / Proof Generation and Compile Repair

For obligations that are not discharged by the cheap arithmetic checker, the Evaluation Agent first generates Lean statements and, when appropriate, then generates Lean proofs\. The agent interacts with Lean through Lean Tools MCP\[[OptSuite, 2026](https://arxiv.org/html/2608.26310#bib.bib14)\], using the returned compilation diagnostics, goal states, and proof\-attempt results as feedback for repair\. The key point here is not the MCP interface itself, but the agentic loop that separates statement generation, semantic checking, and proof generation\.

The statement and proof stages are separated\. A compiled Lean statement is not enough, because it may be semantically unfaithful\. Conversely, an unproved Lean statement is not evidence that the natural\-language obligation is false, since proof search may fail for engineering reasons\. The agent first searches for a compilable and faithful statement; only after the semantic gate is passed does it enter proof generation\.

The statement\-generation loop alternates between Lean compilation and semantic checking\. If Lean reports a syntax, type, import, dependency, namespace, or elaboration error, the next prompt contains the current candidate and MCP diagnostics, and the model is asked to repair only the Lean artifact\. If the candidate compiles, the semantic checker compares it againstmmunderCC\. When semantic drift is detected, the structured semantic report is appended to the next statement\-generation prompt, and the agent revises the formal statement while preserving the original obligation\. The loop terminates when a candidate both compiles and passes the faithfulness gate, or when the budget is exhausted\.

The proof\-generation loop starts only from a compiled and faithful statement\. The proof agent proposes a Lean proof script, checks it through MCP, and repairs only the proof body according to Lean diagnostics and current goal states\. In this stage the statement is held fixed unless the system explicitly returns to statement generation after a confirmed statement\-level issue\. If proof succeeds, the local result ispassedfor the original\-claim branch\. If the system is running a negation or counterexample branch and that branch is verified, the local result isrefuted\. Otherwise, timeout, search exhaustion, or unresolved compiler errors produceinconclusive\.

Algorithm 2Statement and proof generation with MCP compile repairInput:Obligation

o=\(κ,m,C,ue,ρ\)o=\(\\kappa,m,C,u\_\{e\},\\rho\); problem

pp; statement budget

BsB\_\{s\}; proof budget

BpB\_\{p\}; faithfulness threshold

τ\\tau
Output:Local result in

\{passed,refuted,inconclusive\}\\\{\\texttt\{passed\},\\texttt\{refuted\},\\texttt\{inconclusive\}\\\}
if*mmis eligible for cheap arithmetic checking*then

return*CheapArithmeticChecker\(mm\)*

prompt←BuildStatementPrompt​\(p,C,o\)\\textit\{prompt\}\\leftarrow\\textsc\{BuildStatementPrompt\}\(p,C,o\)

report←∅\\textit\{report\}\\leftarrow\\emptyset

for*i=1,…,Bsi=1,\\ldots,B\_\{s\}*do

m^←GenerateLeanStatement​\(prompt,report\)\\hat\{m\}\\leftarrow\\textsc\{GenerateLeanStatement\}\(\\textit\{prompt\},\\textit\{report\}\)
cr←MCP\.lean\_run\_code​\(m^\)\\textit\{cr\}\\leftarrow\\textsc\{MCP\.lean\\\_run\\\_code\}\(\\hat\{m\}\)
if*crhas Lean errors*then

diag←MCP\.lean\_diagnostic\_messages​\(m^\)\\textit\{diag\}\\leftarrow\\textsc\{MCP\.lean\\\_diagnostic\\\_messages\}\(\\hat\{m\}\)
prompt←AddCompileDiagnostics​\(prompt,diag\)\\textit\{prompt\}\\leftarrow\\textsc\{AddCompileDiagnostics\}\(\\textit\{prompt\},\\textit\{diag\}\)
else

report←SemanticChecker​\(m,m^,C\)\\textit\{report\}\\leftarrow\\textsc\{SemanticChecker\}\(m,\\hat\{m\},C\)
if*report\.Sfaith≥τ\\textit\{report\}\.S\_\{\\mathrm\{faith\}\}\\geq\\tauand no critical drift*then

gotoproof stage

else

prompt←AddSemanticReport​\(prompt,report\)\\textit\{prompt\}\\leftarrow\\textsc\{AddSemanticReport\}\(\\textit\{prompt\},\\textit\{report\}\)
return*inconclusivewith statement\-generation diagnostics*

proof stage:

branch←SelectBranch​\(o,suspicion prior\)\\textit\{branch\}\\leftarrow\\textsc\{SelectBranch\}\(o,\\textit\{suspicion prior\}\)

pprompt←BuildProofPrompt​\(p,C,o,m^,branch\)\\textit\{pprompt\}\\leftarrow\\textsc\{BuildProofPrompt\}\(p,C,o,\\hat\{m\},\\textit\{branch\}\)

for*j=1,…,Bpj=1,\\ldots,B\_\{p\}*do

π←GenerateLeanProof​\(pprompt\)\\pi\\leftarrow\\textsc\{GenerateLeanProof\}\(\\textit\{pprompt\}\)
pr←MCP\.lean\_run\_code​\(m^,π\)\\textit\{pr\}\\leftarrow\\textsc\{MCP\.lean\\\_run\\\_code\}\(\\hat\{m\},\\pi\)
if*prsucceeds*then

if*branch=original\\textit\{branch\}=\\texttt\{original\}*then

return*passedwith Lean artifact and faithfulness score*

else

return*refutedwith Lean artifact and faithfulness score*

diag←MCP\.lean\_diagnostic\_messages​\(π\)\\textit\{diag\}\\leftarrow\\textsc\{MCP\.lean\\\_diagnostic\\\_messages\}\(\\pi\)
goals←MCP\.lean\_goal\\textit\{goals\}\\leftarrow\\textsc\{MCP\.lean\\\_goal\}when available

pprompt←AddProofDiagnostics​\(pprompt,diag,goals\)\\textit\{pprompt\}\\leftarrow\\textsc\{AddProofDiagnostics\}\(\\textit\{pprompt\},\\textit\{diag\},\\textit\{goals\}\)
return*inconclusivewith proof\-search diagnostics*

This two\-loop design keeps failed Lean interactions conservative\. Statement compilation errors are treated as formalization failures; semantic drift is treated as an unfaithful artifact; proof failure is treated as insufficient formal evidence\. Only a proof or refutation of a statement that has passed the faithfulness gate becomes strong local evidence for first\-error localization\.

## Appendix DProofLoc Dataset

### D\.1Dataset Summary and Source Provenance

This section supplements the dataset discussion in Section[5](https://arxiv.org/html/2608.26310#S5)\. We evaluate on two expert\-verified benchmarks\.ProofLoc\-Olympiadcontains 350 olympiad\-style algebra and number\-theory problems\.ProofLoc\-Universitycontains 200 university\-level problems across topology and metric spaces, linear algebra, abstract algebra, real analysis, convex analysis, and convex optimization\.

In both datasets, candidate proofs are generated as numbered step\-by\-step natural\-language proofs\. Gold labels are expert judgments aligned to benchmark\-level coarse proof steps rather than to the internalEdgeUnitsused byFaithSieve\. Table[6](https://arxiv.org/html/2608.26310#A4.T6)reports the textbook provenance forProofLoc\-University, making the six\-domain coverage auditable\.

Table 6:Textbook provenance ofProofLoc\-University\.
### D\.2Data Generation

Candidate proofs are generated by GPT\-4o as numbered step\-by\-step proofs\. The generation prompt asks the model to produce a complete proof, not to intentionally produce an incorrect solution\. Thus, the errors in the benchmark arise from naturally occurring model reasoning failures and are then identified by expert annotation\. This setting is intended to capture proof\-step errors that occur during ordinary proof generation, rather than errors produced by adversarial perturbation\.

Each generated proof is annotated by mathematics Ph\.D\. students from well\-known universities\. Annotators are instructed to judge proof correctness at the benchmark step level and to mark the earliest step that introduces a material proof break; correct proofs are labeled ascorrect\. When annotators encounter disagreement or ambiguity, the example is not resolved by a single unilateral label\. Instead, the annotators jointly review the problem statement, the generated proof, the candidate first\-error positions, and the downstream dependence of later steps on the disputed claim\. The final label is assigned only after this adjudication process reaches agreement on whether the disputed step is mathematically recoverable or constitutes the first unrepaired error in the proof\.

Proof Generation Prompt

Writeanumbered,step\-by\-stepproof\.

Eachstepshouldcontainaclearmathematicalinference\.

Donotskipimportantreasoningsteps\.

Problem:

\{problem\}

## Appendix EHuman Audits of Pipeline Components

### E\.1Human Audits of Local Reasoning Construction

#### Decomposition preservation\.

We audited 50 original proof\-decomposition logs to test whether the fine\-grained decomposition preserved the first error in the source proof\. Two independent human experts found preservation in 42/50 \(84%\) and 43/50 \(86%\) proofs, respectively\. In their initial judgments, they agreed that 41 decompositions were fully reliable and that 6 contained partial decomposition issues\. After jointly reviewing the remaining disagreements and the location of each issue, the consolidated result was 43/50 first\-error preservation\. Some decomposition defects occurred only after the source first error and therefore did not alter the final first\-error location\.

#### Suspicion Search calibration\.

We used a pre\-frozen sample of 50 Olympiad proofs, containing 25 correct and 25 known\-wrong proofs and 752EdgeUnits\. One independent human reviewer blindly labeled each proof and unit without access to Search selections, benchmark labels, Lean/gate results, or final predictions\. After excluding three uncertain unit labels, Search obtained the results in Table[7](https://arxiv.org/html/2608.26310#A5.T7)\.

Table 7:Human calibration of Suspicion Search\.The unit\-level TP/TN/FP/FN counts were 174/425/57/93\. Although the unit\-level recall is moderate, the scheduling objective is proof\-level coverage of the earliest error: Search covered that error in 23 of 25 known\-wrong proofs\.

### E\.2Human Calibration of the Semantic Gate

Two independent human experts blindly reviewed 135 evaluable theorem/lemma statements from historical execution records\. Each generated statement was compared with its natural\-language obligation and local context, and disagreements were resolved before computing the confusion matrix in Table[8](https://arxiv.org/html/2608.26310#A5.T8)\.

Table 8:Human calibration of the statement semantic gate on 135 statements\.Treating a faithful statement as positive and gate acceptance as the predicted positive, the gate achieved 88\.98% precision and 91\.30% recall\. Its FPR was 65\.00% and its FNR was 8\.70%\. The 13 accepted\-drift cases had overlapping failure modes: added or strengthened assumptions \(5\), vacuous or trivial propositions \(6\), and weakened targets \(5\)\. These results show that the gate substantially agrees with human judgments but is not itself a fidelity guarantee; accepted formal evidence must remain traceable to its source obligation\.

## Appendix FAdditional Experimental Details and Ablations

### F\.1Tree Scale and Scheduling Sparsity

On the complete Olympiad\-350 artifacts, Suspicion Search reduces the set sent to expensive downstream checks as shown in Table[9](https://arxiv.org/html/2608.26310#A6.T9)\.

Table 9:Tree and candidate sizes on the complete Olympiad\-350 artifacts\.Overall, 1,720 of 5,458 EdgeUnits \(31\.51%\) were selected as candidates, and formalization was restricted to this candidate set\. The prefix\-lookback parameter was fixed to 6: each local audit receives the focus unit and up to six preceding fine\-grained units, for a maximum contiguous context of seven units\. This parameter is configurable and is not selected by the LLM\.

### F\.2Direct Judge Baseline

The direct judge baseline is the most direct natural\-language judging baseline in our experiments\. It receives only the problem statement and the original numbered proof steps, and is asked to outputcorrector the earliest erroneous step number\. It does not use proof decomposition, proof\-state graphs,EdgeUnits, local review, cheap arithmetic checking, Lean validation, semantic gates, or evidence fusion\. This baseline measures the ability of a base model to perform proof correctness judgment and first\-error localization without structured local evidence\.

Each solution is formatted as numbered steps before being inserted into the user message, using the formStep 1: \.\.\.,Step 2: \.\.\.\. The model output is restricted tocorrectorstep N\. During evaluation,correctis parsed as label 0 andstep Nis parsed as the first erroneous stepNN; unparsable outputs are counted as parse failures\.

Direct Judge Baseline Prompt

Youareamathematicalreasoningevaluator\.Givenamathproblemanda

step\-by\-stepsolution,yourtaskistoidentifywhetherthesolutioncontains

anerrorand,ifso,whichstepfirstintroducestheerror\.

Rules:

\-Carefullycheckeachstepformathematicalcorrectness\.

\-Astepisincorrectifitcontainsawrongequation,invalidlogical

deduction,unjustifiedclaim,oraconclusionthatdoesnotfollowfrom

previoussteps\.

\-ReporttheFIRSTstepwhereanerrorappears\.

\-Ifallstepsarecorrect,report"correct"\.

Outputformat\(respondwithONLYoneofthese,nothingelse\):

\-Ifallstepsarecorrect:correct

\-IfstepNisthefirsterror:stepN

Userprompttemplate:

Problem:

\{problem\}

Solutionsteps:

\{steps\}

Identifythefirsterror\.RespondwithONLY"correct"or"stepN"

\(whereNisthestepnumber\)\.

### F\.3FaithSieve Pipeline Settings

The fullFaithSievepipeline includes proof decomposition, proof\-state graph construction,EdgeUnitconstruction, suspicion\-guided scheduling, typed obligation discovery, EvaluationAgent validation, and evidence fusion\. Different backbones use the same task definition, the same benchmark labels, and the same final output format:corrector the earliest erroneous benchmark\-level proof step\. Since benchmark labels are attached to the original proof steps rather than to internalEdgeUnitsor Lean obligations, the final stage maps obligation\-level evidence back to the original step index\.

All LLM calls are issued through OpenAI\-compatible APIs or the corresponding provider APIs\. Closed or hosted frontier models are queried through their provider endpoints\. Qwen3\.5\-9B is deployed as an OpenAI\-compatible endpoint using SGLang on a single NVIDIA H100 80G GPU\. The experimental pipeline does not use an external coding\-agent framework; models receive prompts through APIs and return text responses\. Lean file creation, file editing, snippet checking, diagnostics, proof\-state inspection, and timeout\-controlled validation are performed throughlean\-tools\-MCP\.

Lean validation is performed on CPU\. For each local obligation sent to the Formal Evaluation Agent, the system first generates a Lean statement and checks whether it compiles\. Only after the statement passes the semantic gate does the system attempt proof, refutation, or counterexample search\. The Lean proof loop uses a 10\-minute timeout\. This threshold is intentionally permissive because the checked targets are local obligations produced after decomposition, such as algebraic rewrites, derived facts, goal reductions, witness checks, case\-split subgoals, or simple entailments\. A timeout is treated as inconclusive formal evidence rather than as direct evidence that the original proof step is wrong\.

### F\.4Full Main Results

Table[10](https://arxiv.org/html/2608.26310#A6.T10)reports the full main results corresponding to Section[5](https://arxiv.org/html/2608.26310#S5)\. Exact accuracy requires the predicted first erroneous step to match the benchmark label exactly, while binary accuracy evaluates only the correct\-versus\-incorrect decision\. TheFaithSieverows in this table denote complete end\-to\-end pipeline runs\.

Table 10:MainFaithSieveresults\.
### F\.5Ablation Study and Analysis

The ablation experiments evaluate the contribution of individual components by preserving or removing specific parts of theFaithSievepipeline\. Whenever possible, the experiments reuse intermediate artifacts produced by the full pipeline and replay the downstream synthesis or validation stages affected by the ablated component\. This design makes the ablations closer to component diagnosis: the comparison asks what changes when a specific source of evidence is removed or weakened, while reducing variation from rerunning earlier LLM\-based stages\.

Table[11](https://arxiv.org/html/2608.26310#A6.T11)summarizes the component configuration of each ablation variant, and Table[12](https://arxiv.org/html/2608.26310#A6.T12)reports the corresponding results onProofLoc\-Olympiad\. The table omits an interpretation column so that the numeric comparison remains explicit; the following paragraphs discuss the mechanism tested by each variant\.

Table 11:Component configuration of ablation variants\.Table 12:Ablation results onProofLoc\-Olympiad\.The direct\-judge baseline removes the entire structured\-evidence pipeline\. It reads the problem statement and the original numbered proof steps, then predictscorrector the first erroneous step in a single pass\. GPT\-5\.4 direct judging obtains 72\.29% exact / 88\.29% binary accuracy, while Qwen3\.5\-9B obtains 53\.71% exact / 76\.00% binary accuracy\. The gap to the full setting indicates that first\-error localization benefits from organizing the proof into local evidence\-bearing units rather than relying only on whole\-proof natural\-language judgment\.

The Step3 graph judge keeps the decomposition and proof\-state graph artifacts, but removes local EdgeUnit review, typed obligation discovery, Lean validation, and final evidence fusion\. This variant tests whether tree\-level organization alone can improve localization\. It improves over direct judging for both backbones, reaching 75\.71% exact / 88\.57% binary with GPT\-5\.4 and 65\.71% exact / 77\.71% binary with Qwen3\.5\-9B\. The improvement is larger for exact accuracy than for binary accuracy, suggesting that the graph mainly helps identify where the reasoning first goes wrong, while still lacking the local verification evidence needed by the full system\.

The EdgeUnit \+ NL only variant keeps local EdgeUnit\-level review and final synthesis, but disables the Formal Evaluation Agent, including cheap arithmetic checking, Lean statement generation, Lean validation, and the semantic gate for formal evidence\. With GPT\-5\.4 it obtains 73\.43% exact / 88\.00% binary accuracy; with Qwen3\.5\-9B it obtains 71\.14% exact / 86\.00% binary accuracy\. The strong improvement for Qwen3\.5\-9B shows that local EdgeUnit representations help a smaller backbone focus on checkable transitions even without formal validation, although this setting remains below the full replay result\.

The locality ablation removes local EdgeUnits and falls back to coarse\-step\-level evidence units\. GPT\-5\.4 drops to 60\.86% exact / 72\.29% binary accuracy, and Qwen3\.5\-9B obtains 62\.29% exact / 77\.71% binary accuracy\. This is the largest degradation among the reported variants\. The result supports the locality hypothesis: benchmark steps are annotation units, but they are often too coarse to serve as reliable reasoning units\. Decomposing them into local transitions is therefore essential for detecting the first material proof break\.

The semantic\-gate ablation keeps hybrid validation but disables or loosens the statement\-faithfulness filter before formal evidence is admitted into the final evidence set\. GPT\-5\.4 with w/o semantic gate obtains 70\.86% exact / 86\.29% binary accuracy, and Qwen3\.5\-9B obtains 70\.86% exact / 86\.00% binary accuracy\. These drops show that a Lean proof or checker success is useful only when the generated formal statement remains aligned with the original natural\-language obligation\. Without the semantic gate, formally valid but semantically shifted statements can contaminate the final judgment\.

### F\.6Label Balance and End\-to\-End Error Decomposition

ProofLoc\-Olympiadcontains 153 correct and 197 incorrect proofs;ProofLoc\-Universitycontains 130 correct and 70 incorrect proofs\. Table[13](https://arxiv.org/html/2608.26310#A6.T13)reports the complete GPT\-5\.4 confusion matrices\. We treat an incorrect proof as the positive class: FP is a correct proof flagged as incorrect, and FN is an incorrect proof accepted as correct\.

Table 13:Complete GPT\-5\.4 correct/incorrect confusion matrices\.FaithSievereduces the false\-positive rate from 21\.57% to 9\.15% on Olympiad and from 16\.92% to 6\.92% on University\. Table[14](https://arxiv.org/html/2608.26310#A6.T14)separates binary errors from cases where the binary verdict is correct but the first\-error position is mislocalized\.

Table 14:Composition of the remaining GPT\-5\.4FaithSieveExact errors\.The largest residual category on both datasets is therefore localization rather than binary proof classification\. On University\-200, the paired Exact table contains 139 cases where both Direct@1 andFaithSieveare correct, 30 where onlyFaithSieveis correct, 11 where only Direct@1 is correct, and 20 where both are wrong\. This separates the 9\.5\-point Exact gain over Direct@1 from the remaining 15\.5\-point gap to perfect localization\.

### F\.7Multi\-Sample, Deliberative, and External Baselines

We added multi\-sample direct judging and a deliberative baseline under the same first\-error localization interface\. Direct@5 aggregates five independent judgments\. The deliberative baseline uses two independent critics followed by one adjudicator\. Within each dataset, all methods use the same problems and backbone: GPT\-5\.4 on the complete University\-200 set and Qwen3\.5\-9B on the tested 200\-example BIG\-Bench Mistake subset\.

Table 15:Additional natural\-language baselines\. The BIG\-Bench Mistake result uses the tested 200\-example subset\.On University Exact,FaithSieveimproves over both Direct@5 and the critic baseline by 8\.5 points\. The paired 95% CI for both comparisons is\[\+2\.5,\+14\.5\]\[\+2\.5,\+14\.5\]and McNemar’sp=0\.00948p=0\.00948\. The corresponding BIG\-Bench Exact gains are 9\.5 and 6\.5 points\.

We also evaluated three public process reward models as*off\-the\-shelf transfer diagnostics*\. Each PRM scores the original proof steps, predicts the first step below its frozen threshold, and predictscorrectif every step passes\. Thresholds were calibrated externally on ProcessBench GSM8K\-400 and frozen before evaluation: 0\.904296875 for Qwen2\.5\-Math\-PRM\-7B, 0\.34375 for Skywork\-o1\-Open\-PRM, and 0\.5007799117379625 for EurusPRM\-Stage2\.

Table 16:Off\-the\-shelf PRM transfer under the same first\-error interface\.This table is not a model\-capability\- or token\-budget\-matched comparison\. It tests whether existing public mathematical PRMs transfer directly to a fixed proof’s first\-error localization task\. Standard Best\-of\-NNinstead ranksNNcandidate solutions\. Here Direct@NNproduces multiple judgments of one fixed proof; a solution\-step PRM applied to that same proof produces the same score vector for every Direct sample\. Applying such a PRM to Direct’s evaluator rationales would instead be an uncalibrated use on evaluator traces, which these PRMs were not trained to score\.

The BIG\-Bench Mistake subset contains 200 examples: 80 Multistep Arithmetic, 60 Tracking Shuffled Objects, and 60 Dyck Languages examples, with 100 correct and 100 incorrect proofs\. It was sampled because a complete end\-to\-end run over all 2,186 examples was not feasible within the available compute budget\.

### F\.8Token Cost and High\-Budget Controls

#### Recorded pipeline cost\.

FaithSieve has high model\-token consumption because it includes agentic formalization and proof generation\. Under a fixed 50\-problem cost\-evaluation setting, total tokens were the unweighted sum of recorded input and output tokens\.

Table 17:Average recorded token consumption in the fixed 50\-problem cost evaluation\.
#### Same\-backbone high\-budget controls\.

We added Direct Majority scaling and two high\-budget NL\-only agents on all 200 examples of the same pre\-fixed BIG\-Bench Mistake subset\. Every method in Table[18](https://arxiv.org/html/2608.26310#A6.T18)uses the same Qwen3\.5\-9B checkpoint with thinking disabled\. The controls use a 300\-second per\-request timeout; ground truth is joined only after outputs are frozen\. Direct Majority uses temperature 0\.6 and a 64\-token output limit\. The two structured NL\-only agents use temperature 0\.1 and stage\-specific output limits of 64–3072\. Other decoding settings follow service defaults\.

Table 18:Same\-data, same\-backbone token\-budget controls on BIG\-Bench\-200\.Direct Majority@NNaggregates normalized labels in\{correct,step​k\}\\\{\\texttt\{correct\},\\texttt\{step \}k\\\}by plurality\. Ties select the earliest numeric step;correctis selected only when it is the unique top label\. ForN<241N<241, entries are means over 1,000 fixed\-seed samples without replacement from a frozen 241\-vote pool;N=241N=241uses the complete pool\. The slight decline with largerNNreflects systematic modal bias rather than an aggregation anomaly: 90/200 problems receive the same label in all 241 samples, another 44 contain the gold label but not as the modal label, and there are no modal ties atN=65,129,N=65,129,or 241\.

The Context\-Isolated Reviewer Panel creates three independent roles: validity, localization, and counterexample review\. Each role contains 32 separately sampled reviewers with isolated contexts, followed by role summaries, two adjudication rounds, final synthesis, consistency checking, and label normalization\. The NL\-Only Decomposition \+ Challenge\-Defense agent decomposes the proof while retaining source\-step mappings, selects at most four candidate first errors, runs challenger/defender/judge analysis plus 12 independent audits per candidate, and then performs global consistency, critique, revision, and final synthesis\. Neither agent uses Lean, a PRM, or FaithSieve artifacts\.

These controls do not make FaithSieve inexpensive\. Instead, they show that on the same data and backbone, reallocating a comparable token budget to repeated natural\-language judgments or structured NL\-only agents did not reproduce the gain from adding locally checkable Lean evidence\.

### F\.9Domain\-Level Uncertainty

We report the repeated domain\-level analysis on University\-200\. Table[19](https://arxiv.org/html/2608.26310#A6.T19)gives sample sizes and two\-sided Wilson 95% confidence intervals for Exact accuracy\. All methods use GPT\-5\.4; the FaithSieve point estimates are the original University\-200 results\.

Table 19:University\-200 Exact accuracy with two\-sided Wilson 95% confidence intervals\.FaithSieve is relatively high on Linear Algebra and Abstract Algebra\. A plausible explanation is that these domains often expose clearer algebraic objects, theorem dependencies, and local derivation structures, which align well with fine\-grained decomposition, statement formalization, and Lean verification\. The intervals remain important because several domains contain only 20–40 examples\.

### F\.10Decoding Configuration of the Original University Experiment

Table[20](https://arxiv.org/html/2608.26310#A6.T20)reports the frozen stage\-specific settings of the original University\-200 experiment\. It does not mix in configurations from additional baselines\. Output limits are reported only where they were explicitly set at the call site; otherwise the provider default was used\.

Table 20:Decoding configuration of the original University\-200 experiment\.The shared settings were:top\_p, request seed, frequency penalty, presence penalty, and stop all used provider defaults\. These settings were fixed throughout the complete University\-200 evaluation\.

## Appendix GLimitations and Broader Impacts

### G\.1Limitations

Although our method improves exact and binary accuracy for first\-error localization onProofLoc\-Olympiad, it is limited by the cost and coverage of formal validation\. Lean\-assisted verification involves statement generation, compile repair, proof search, artifact checking, and evidence normalization; any stage may fail or time out\. The method also depends on current LLM agents for autoformalization and proof repair, so unfamiliar Lean representations or mismatches between mathlib definitions and natural\-language conventions can turn an otherwise checkable claim into inconclusive evidence\.

A second limitation is domain coverage\.ProofLoc\-Olympiadfocuses on algebra and number theory, where local transformations often form clear typed obligations\. Geometry and combinatorics require diagrammatic objects, construction relations, counting models, and problem\-specific encodings, so failures may reflect modeling choices or library coverage\.ProofLoc\-Universityexpands the evaluation to six abstract domains, but broader university\-level mathematics still requires additional annotation and verification\.

### G\.2Broader Impacts

This work aims to move mathematical reasoning systems from producing plausible final answers toward providing local evidence that is traceable, checkable, and interpretable\. Such evidence may support more reliable AI proof assistants, step\-level feedback in mathematical education, quality control for generated proofs, and better interfaces between informal mathematical writing and formalized mathematics\.

At the same time,FaithSieveshould not be viewed as an automatic replacement for human mathematical judgment\. It is better understood as an auditing aid: it helps identify high\-risk proof steps, filters unfaithful formalizations, and organizes checkable evidence in the context of the original proof\. In educational settings, this distinction is especially important: local feedback should help students inspect and repair reasoning, rather than simply assign authoritative correctness labels\.

The main risk is over\-reliance on incomplete formal evidence\. A successful Lean proof is useful only when the generated statement faithfully represents the original obligation, and an inconclusive result does not imply that the proof step is wrong\. For this reason, the system explicitly separates semantic faithfulness, formal validation status, and final benchmark\-level prediction\. We expect responsible uses to preserve this evidence trail and to present uncertain cases as uncertain, especially in high\-stakes mathematical review or instruction\.

## Appendix HCase Studies: Natural\-Language Context for Representative Lean Statements

The following examples expose the source natural\-language claim, the extracted local obligation, and an ASCII\-rendered Lean target\. The execution records retain the complete problem, full natural\-language proof, source\-step mapping, local context, generated statement, and proof result\. All six proof scripts were rechecked successfully with Lean\. The first two targets prove explicit negations of incorrect source claims; the remaining four prove correct local obligations\. A successful local theorem is evidence only for its corresponding NL–FL pair, not a certificate for the entire proof\.

#### Example 1: polynomial witnesses \(caught error\)\.

The problem asks for the smallest number of rational\-coefficient polynomial squares needed to representX2\+7X^\{2\}\+7\. The source step claims thatf1=X2\+2f\_\{1\}=X^\{2\}\+2andf2=f3=f4=−1f\_\{2\}=f\_\{3\}=f\_\{4\}=\-1satisfy the identity, thereby making four summands feasible\. The local validation target retains all four concrete witnesses and proves that no such instantiation satisfies the asserted identity\.

Not\(Existsfunf1:PolynomialRat=\>

Existsfunf2:PolynomialRat=\>

Existsfunf3:PolynomialRat=\>

Existsfunf4:PolynomialRat=\>

Polynomial\.X^2\+7=f1^2\+f2^2\+f3^2\+f4^2/\\

f1=Polynomial\.X^2\+2/\\

f2=\-1/\\f3=\-1/\\f4=\-1\)

AtX=1X=1, the asserted identity gives 8 on the left and 12 on the right; equivalently, the polynomial coefficient comparison fails because\(X2\+2\)2\(X^\{2\}\+2\)^\{2\}introduces anX4X^\{4\}term\. Lean verifies the negation and the result is mapped back to the source claim\.

#### Example 2: quadratic coefficient \(caught error\)\.

The local context containsT=8T=8,c/a=Tc/a=T, the point\-value equationsf⁡\(−2\)=20f\(\-2\)=20andf⁡\(1\)=14f\(1\)=14, and the simplified equations12​a−2​b=2012a\-2b=20and9​a\+b=149a\+b=14\. The source step concludesa=4/3a=4/3; the extracted obligation asks whether that conclusion follows\. The validation branch proves its negation while retaining the inherited equations\.

\(abcT:Real\)\(f:Real\-\>Real\)

\(hT:T=8\)\(hf:forallx,fx=a\*x^2\+b\*x\+c\)

\(hprod:c/a=T\)\(hpt1:f\(\-2\)=20\)\(hpt2:f1=14\)

\(heq1:4\*a\-2\*b\+c=20\)

\(heq2:a\+b\+c=14\)

\(hcrel:c=8\*a\)

\(hsimp1:12\*a\-2\*b=20\)

\(hsimp2:9\*a\+b=14\):

Not\(a=4/3\)

Adding twice the second simplified equation to the first yields30​a=2430a=24, so the consistent value isa=4/5a=4/5, not4/34/3\.

#### Example 3: functional equation \(proved local step\)\.

The problem givesf⁡\(2​x\+3\)=2​f​\(x\)\+3f\(2x\+3\)=2f\(x\)\+3andf⁡\(0\)=6f\(0\)=6\. After derivingf⁡\(3\)=15f\(3\)=15, the source step substitutesx=3x=3and concludesf⁡\(9\)=33f\(9\)=33\. The theorem keeps the recurrence, initial value, and previously derived local fact\.

\(f:Real\-\>Real\)

\(hprop:forallx,f\(2\*x\+3\)=2\*fx\+3\)

\(hbase:f0=6\)\(hf3:f3=15\):

f9=33

#### Example 4: logarithm change of base \(proved local step\)\.

The source proof rewriteslog4⁡x\\log\_\{4\}xas12​log2​x\\tfrac\{1\}\{2\}\\log\_\{2\}xwhile solving a three\-equation logarithmic system\. The local statement retains positivity and the original system rather than checking an isolated identity without its proof context\.

\(xyz:Real\)\(hx:x\>0\)\(hy:y\>0\)\(hz:z\>0\)

\(hsys:Real\.logb4x\+Real\.logb8\(y\*z\)=2/\\

Real\.logb4y\+Real\.logb8\(x\*z\)=4/\\

Real\.logb4z\+Real\.logb8\(x\*y\)=5\):

Real\.logb4x=\(1/2\)\*Real\.logb2x

#### Example 5: real\-exponentiation rewrite \(proved local step\)\.

The source equation is2x\+2​56−x=10x22^\{x\+2\}5^\{6\-x\}=10^\{x^\{2\}\}\. The local obligation checks the rewrite of the right\-hand side into2x2​5x22^\{x^\{2\}\}5^\{x^\{2\}\}while retaining the original equation as an assumption\.

\(hgiven:\(2:Real\)^\(x\+2\)\*\(5:Real\)^\(6\-x\)=

\(10:Real\)^\(x^2\)\):

\(2:Real\)^\(x\+2\)\*\(5:Real\)^\(6\-x\)=

\(2:Real\)^\(x^2\)\*\(5:Real\)^\(x^2\)

#### Example 6: integer arithmetic \(proved local value\)\.

In BIG\-Bench Mistake example 71, the source proof computesB=0⋅5−\(−1\)−\(−5\)=6B=0\\cdot 5\-\(\-1\)\-\(\-5\)=6\. The extracted statement has the same concrete arithmetic target and is discharged by normalization\.

\(0:Int\)\*5\-\(\-1\)\-\(\-5\)=6