Evaluating Research-Level Math Proofs via Strict Step-Level Verification

# Evaluating Research-Level Math Proofs via Strict Step-Level Verification
Source: [https://arxiv.org/html/2606.10799](https://arxiv.org/html/2606.10799)
###### Abstract

Large Language Models \(LLMs\) struggle to rigorously verify complex mathematical proofs\. Standard global evaluation approaches suffer from “context poisoning,” in which superficially plausible statements mask subtle logical flaws, leading to hallucination or over\-skepticism\. To address this, we shift from global evaluation to strict step\-level verification: our framework maintains detailed context for each deduction step and strictly constrains the sources of applied theorems\. We evaluate on a carefully curated adversarial diagnostic suite of research\-level proofs drawn from the FirstProof challenge\. A systematic ablation study demonstrates that these deductive constraints are indispensable, as unconstrained global prompting consistently fails to localize subtle logical errors\. Beyond outperforming global evaluation, our approach fundamentally alters the failure taxonomy\. Error analysis reveals that, rather than exhibiting severe logical hallucinations, remaining rejections are primarily instances of “pedantic hyper\-rigor” stemming from unstated domain conventions, effectively exposing implicit ambiguities within the expert benchmark itself\. Our findings suggest that prompting agents to organize their verification notes in a cautious, human\-mathematician\-like manner can substantially improve their ability to distinguish rigorous proofs from flawed ones, with the potential to strengthen agentic reasoning on frontier mathematical concepts that the base model does not already know well, and to lay a theoretical foundation for future automated proof\-review systems\. Code and prompts are available at[GitHub](https://github.com/celainica/A-lightweight-natural-language-proof-verification-agent)\.

## 1Introduction

The self\-correction and reasoning capabilities of Large Language Models \(LLMs\) and AI agents have improved significantly with scaling and reinforcement learning\[[7](https://arxiv.org/html/2606.10799#bib.bib19)\]\. In the mathematical domain, agent frameworks have demonstrated impressive problem\-solving results\[[8](https://arxiv.org/html/2606.10799#bib.bib6),[14](https://arxiv.org/html/2606.10799#bib.bib5)\]\. However, when verifying research\-level mathematical proofs, current models frequently falter\. Standard global evaluation approaches often suffer from “context poisoning,” where superficially plausible statements mask subtle spurious justifications, leading agents to either hallucinate validity or exhibit over\-skepticism\.

While formal verification systems such as Lean\[[6](https://arxiv.org/html/2606.10799#bib.bib2)\]offer absolute guarantees, their application is bottlenecked by human\-built infrastructures and a heavy reliance on manually maintained libraries \(e\.g\.,Mathlib\[[21](https://arxiv.org/html/2606.10799#bib.bib12)\]\)\. This naturally constrains the ability of current automated agents to formally verify advanced mathematical concepts\. Therefore, verifying proofs in natural language remains an essential frontier\. Generating fine\-grained elaborations of informal proofs serves as a crucial bridge: it not only aids human mathematicians in peer review but also assists agentic systems in eventually translating informal math into rigorous formal code\[[23](https://arxiv.org/html/2606.10799#bib.bib13),[13](https://arxiv.org/html/2606.10799#bib.bib14),[3](https://arxiv.org/html/2606.10799#bib.bib15),[24](https://arxiv.org/html/2606.10799#bib.bib16),[25](https://arxiv.org/html/2606.10799#bib.bib17)\]\.

Crucially, this focus on AI self\-correction serves a fundamentally different role than formalization itself\. Formal verification systems operate on a paradigm of ultimate accountability, where the underlying infrastructure \(e\.g\., Lean\) or a human expert bears the responsibility of providing an absolute guarantee of correctness\. In contrast, our objective is to equip the agent with an intrinsic capacity to distinguish sound reasoning from flawed logic during its exploratory and generative phases\. After all, agents will inevitably encounter scenarios where they must rely entirely on pure natural language reasoning to conceptualize and discover solutions\. In the highly unconstrained search space of mathematical discovery, enabling an agent to recognize its own missteps is critical for pruning dead ends and drastically reducing the generation of hallucinatory or structurally flawed proofs\. Ultimately, we aim to demonstrate a core principle of agentic reasoning:by forcing a model to explicitly and exhaustively write out the underlying details of an informal proof, we inherently amplify its ability to discover subtle logical errors that its standard reasoning would otherwise gloss over\. It is important to emphasize that, to validate our approach, we merely task the agent with the process of elaboration rather than demanding a flawlessly exhaustive natural language proof as the final output\. Consequently, our objective is not to reinvent de Bruijn’s Mathematical Vernacular \(MV\)\. Rather, we aim to demonstrate that agents—much like human mathematicians—leverage the very act of detailed writing to ascertain which conclusions are genuinely correct and rigorously proven\.

To achieve this, we aim to design an agent framework that evaluates proofs with the strictness of a human mathematician reviewing a manuscript\. Such a system must prioritizesoundness\(eliminating false acceptances of flawed proofs\) over mere completeness, and effectivelyleverage inference\-time computeto achieve greater clarity the longer it reasons\. We introduce a crucial methodological shift:reframing verification from direct anomaly detection to constructive elaborationviastrict step\-level verification\. Rather than directly querying an LLM to spot flaws within a global context—a task highly susceptible to context poisoning and hallucination—we test whether the proof can be rigorously and explicitly expanded\. For a mathematical textSStreated as a string, we decompose it into an ordered sequence ofsteps\(s1,s2,…,sn\)\(s\_\{1\},s\_\{2\},\\dots,s\_\{n\}\), isolatingdeduction stepsthat contain logical assertions\. By “elaborating a step,” we mean expanding a deduction stepsis\_\{i\}into a finer\-grained derivation stringsi′s\_\{i\}^\{\\prime\}in natural language that strictly preserves the original reasoning trajectory but explicitly unpacks the underlying logic\. Consequently, anomaly detection emerges naturally from the generative process: if an agent fails to construct a validsi′s\_\{i\}^\{\\prime\}, we suspectsis\_\{i\}harbors a logical gap or unsound justification\. By forcing the agent to elaborate, we replace the LLM’s opaque internal judgments with strict generation constraints\[[15](https://arxiv.org/html/2606.10799#bib.bib4),[4](https://arxiv.org/html/2606.10799#bib.bib18)\]\. Every elaborated step is required to explicitly ground its applied theorems and logical derivations, reducing superficial plausibility\.

To systematically enforce these constraints and ensure the elaboration does not introduce hallucinations of its own, we ground our process in a formal descriptive framework\. Specifically, we model the logical dependencies of any deduction step using a rigorous tripartite architecture:internal context\(Γi\\Gamma\_\{i\}, encompassing theorems, definitions, and hypotheses directly originating from the proof textSS\),external knowledge\(Σi\\Sigma\_\{i\}, comprising non\-trivial statements drawn from outside literature or established domain consensus\), andbackground theory\(𝒯i\\mathcal\{T\}\_\{i\}, representing trivial statements or rewrite rules necessary to syntactically derive the assertion\)\.

Operationally, we implement this step\-level verification as an autonomous, state\-driven agentic workflow guided by fixed prompt files\. By default, every deduction stepsis\_\{i\}is initialized with a conservative local status\. During each iteration, the agent attempts to elaborate the remainingopensteps\. Based on the strict\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)constraints, the agent executes specific state transition actions: if an elaboration is successfully derived, the step transitions toverified; conversely, if the agent identifies a distinct logical error, it flags the step asflawed\. To rigorously guard against false positives \(i\.e\., pedantic over\-rejection\), anyflawedstep triggers a fixed confirmation phase: the agent attempts to confirm the error, potentially reverting the state back toopenif the perceived flaw is resolved upon re\-evaluation\. This iterative process is governed by strict halting criteria: \(1\)Acceptance:the proof is deemed valid if and only if all steps reach theverifiedstate; \(2\)Rejection:the process terminates immediately and rejects the proof if aflawedstate is definitively confirmed upon reflection; and \(3\)Exhaustion:to prevent infinite loops on intractable gaps, the system globally halts and rejects the proof after five consecutive reasoning resumptions without an observed progress signal\.

To empirically validate our proof of concept and demonstrate its potential reward, we construct a highly curated diagnostic suite of challenging mathematical proofs\. We focus on a small\-scale sample to ensure absolute clarity in our evaluation: every proof has been meticulously verified by human experts to establish an unambiguous ground truth, classifying them as either strictly valid or explicitly invalid\. Specifically, our diagnostic suite is heavily anchored in theFirstProofchallenge\[[1](https://arxiv.org/html/2606.10799#bib.bib1),[9](https://arxiv.org/html/2606.10799#bib.bib8),[10](https://arxiv.org/html/2606.10799#bib.bib7)\]\. To establish an unambiguous ground truth, we collected proofs that have undergone rigorous expert evaluation, securing a highly curated collection of 21 research\-grade proofs definitively classified as either strictly valid or explicitly invalid\. These 21 samples are strategically drawn from three authoritative sources: \(1\) official FirstProof releases, \(2\) correct proofs generated by the Aletheia, and \(3\) generations from OpenAI’s solutions\. By anchoring our evaluation on this precise, expert\-verified suite, we can investigate how our step\-level verification effectively isolates subtle reasoning errors that standard global evaluators consistently miss\.

In our evaluation on the curated 21\-proof suite, we observe that current large language models demonstrate strong capabilities in standard contexts: the standard global baseline successfully identified the logical errors in 8 out of the 10 explicitly invalid proofs\. However, a detailed analysis of the remaining 2 cases where the global pipeline failed reveals a specific vulnerability\. In these specific cases, the flawed proofs package incorrect mathematical knowledge—which the LLM is unfamiliar with—into structurally rigorous and plausible formats\. This empirical result highlights that proof verification remains a highly challenging task, particularly for novel or frontier mathematics where LLMs lack prior familiarity with the specific domain knowledge and can be easily deceived by formal\-sounding pseudoproofs\.

To address this limitation, we evaluated our step\-level verification agent under a strict avg@3 setting, supplemented by multi\-pass experiments on these specific adversarial examples\. By explicitly grounding the reasoning process within the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)constraints to trace external knowledge, our framework successfully isolated these camouflaged errors, successfully rejecting all invalid proofs\. Furthermore, out of the valid proofs, our agent failed to verify only 3 cases\. Paradoxically, these failures highlight the meticulousness of our framework\. The agent did not fail due to logical reasoning deficits, but because the underlying base model lacked familiarity with highly specific domain conventions, where certain mathematical objects inherently possess implicit properties by default\. Consequently, it failed to establish the necessary prerequisite statements for the local context\.

For example, in Question 7 of the FirstProof dataset, a human expert naturally assumes that the subgroupΓ\\Gammais explicitly linear \(since it is a subgroup of a real semi\-simple Lie group, and by convention within this specific research domain, such groups are treated as linear\)\[[10](https://arxiv.org/html/2606.10799#bib.bib7),[22](https://arxiv.org/html/2606.10799#bib.bib9)\]\. While the standard baseline simply ignored this subtle leap and glossed over the text, our agent rigorously noted that under the general definition, a subgroup of a real semi\-simple Lie group is not necessarily linear by default\[[19](https://arxiv.org/html/2606.10799#bib.bib20)\]\. Because the base model was unfamiliar with this established domain convention, it conservatively refused to arbitrarily add the linearity assumption into the local context, ultimately losing a fundamental condition required to verify the proof\. This contrast perfectly demonstrates that our framework enforces genuine deductive verification over superficial pattern matching, even if it halts when confronted with domain\-specific conventions it has not yet mastered\.

In summary, our main contributions are threefold:

- •Methodological Paradigm Shift:We reframe natural language proof verification from direct, black\-box anomaly detection toconstructive elaboration\. By modeling the logical dependencies of deduction steps through a novel\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)tripartite architecture, we force the model to explicitly trace internal contexts, external knowledge, and background theories, thereby mitigating superficial pattern matching\.
- •Autonomous Verification Workflow:We propose a state\-driven agentic framework governed by strict step\-level constraints\. Equipped with a fixed confirmation phase and robust halting criteria, our system prioritizes logical soundness and effectively leverages inference\-time compute to prevent the “context poisoning” that plagues global evaluators\.
- •Empirical Insights via Micro\-benchmarking:Our evaluation demonstrates that while even highly capable standard baselines can still be deceived by structurally rigorous pseudoproofs, our framework achieves zero false acceptances on the problem set\. Furthermore, our qualitative analysis reveals a critical bottleneck in current verification tasks: the vulnerability of base models to unstated, domain\-specific hidden conventions\.

## 2Related Work

#### Math Agents

Agentic frameworks for mathematics have advanced rapidly and are producing more and more significant results in research\-level mathematics\. These agents may or may not utilize proof assistants and formal languages\. Recent frontier breakthroughs have heavily favored second paradigm: agents conduct exploration, reasoning, and proof construction entirely in pure natural language\. For instance,Rethlas\[[14](https://arxiv.org/html/2606.10799#bib.bib5)\]can operate as an informal reasoning agent that mimics human mathematical workflows—exploring literature and proposing candidate natural\-language proofs for advanced open problems\. Similarly,Aletheia\[[8](https://arxiv.org/html/2606.10799#bib.bib6)\]functions as an end\-to\-end natural language research agent capable of iteratively generating, verifying, and revising solutions from PhD\-level exercises to autonomous research papers\. Most recently,OpenAI’s model\[[20](https://arxiv.org/html/2606.10799#bib.bib24)\]achieved a historic milestone by disproving Erdős’s 80\-year\-old planar unit distance conjecture using highly complex, purely informal reasoning\. However, despite their immense generative power, a critical vulnerability of these pure natural language agents is their susceptibility to hallucinations and subtle logical gaps, particularly when self\-evaluating long\-horizon mathematical proofs\.\[[18](https://arxiv.org/html/2606.10799#bib.bib21),[17](https://arxiv.org/html/2606.10799#bib.bib22),[16](https://arxiv.org/html/2606.10799#bib.bib23)\]Our work directly addresses this vulnerability\. We demonstrate a structured pathway for pure natural language agents to independently overcome these blind spots: by enforcing strict, step\-level detailed elaboration, agents can systematically unpack their reasoning, rigorously detect anomalies, and eliminate hallucinations without needing to fall back on external formalization infrastructures\.

#### Mathematical Vernacular

The conceptual ambition of bridging informal human mathematical discourse and strict mechanical logic dates back to de Bruijn’s Mathematical Vernacular \(MV\)\[[5](https://arxiv.org/html/2606.10799#bib.bib3)\]\. MV was proposed as an intermediate representational language that obeys formal grammatical rules while preserving the natural “resting points” \(steps\) of mathematical reasoning, thus serving as a stepping stone toward fully coded formal systems \(e\.g\., Automath\)\. Importantly, we do not intend to replicate MV or construct a rigid natural\-language proof assistant\. Rather, we adopt its underlying philosophy to help autonomous agents systematically reduce logical hallucinations\. By structuring natural language proofs around the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)tuple extraction, our framework computationally isolates these resting points, bringing rigor to informal mathematical text\. Crucially, in practice, we do not algorithmically verify whether the agent flawlessly executes this extraction; the mere attempt to engage in this highly structured elaboration is sufficient to expose hidden logical flaws and elevate the agent’s evaluative accuracy\.

## 3Methodology

For a mathematical textSStreated as a string, it can naturally be decomposed into an ordered sequence of steps\(s1,s2,…,sn\)\(s\_\{1\},s\_\{2\},\\dots,s\_\{n\}\)\. Unlike fully formalized proofs in systems like Lean or Rocq\[[6](https://arxiv.org/html/2606.10799#bib.bib2),[21](https://arxiv.org/html/2606.10799#bib.bib12)\], natural language mathematical proofs inherently omit trivial algebraic manipulations and elementary logical deductions to maintain readability\. Because of these inherent omissions, evaluating a proof as a monolithic global text often obscures subtle flaws and logical gaps\.

To address this, we reframe verification from direct anomaly detection toconstructive elaboration\. By “elaborating a step”, we mean that for a given deduction stepsis\_\{i\}with an assertion \(derived conclusion statement\)aia\_\{i\}, we provide an expanded derivationsi′s\_\{i\}^\{\\prime\}that concludes with the identical assertion assis\_\{i\}\. Crucially,si′s\_\{i\}^\{\\prime\}must strictly preserve the original reasoning trajectory ofsis\_\{i\}, but unpack the logic at a finer granularity\. If we fail to come up with a valid expanded derivation, we suspectsis\_\{i\}to contain a logical gap or flaw\.

### 3\.1The Tripartite Explanation Framework

To systematically investigate whether an elaborationsi′s\_\{i\}^\{\\prime\}successfully bridges a gap without demanding explicit syntactic completeness \(which misaligns with human communication\), we introduce the formal concept of an explanation\.

It is crucial to clarify that this theoretical framework is not artificially engineered solely for AI agents; rather, it stems directly from a refinement of the routine cognitive actions human mathematicians employ when explaining and validating a proof\. By adopting this stance, the framework is sufficientlydescriptiveto ensure universal applicability to human mathematical discourse, while simultaneously providing a rigorous,prescriptivestructure that conveniently facilitates systematical analysis and guides agentic workflows\.\[[12](https://arxiv.org/html/2606.10799#bib.bib25)\]In our implementation, we explicitly prompt the agent to output its elaborations according to the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)tripartite structure\. However, it is worth noting that we do not claim this explicit formatting is necessarily the optimal approach, given the additional generation overhead it imposes on the agent\. Alternative implementations may achieve similar rigor by simply requiring the agent to maintain a detailed, distinct record of internal contexts versus external knowledge, without strictly enforcing the tripartite syntax\.

We model the logical dependencies of any deduction step \(or its elaboration\) using this framework\. We define anexplanationof the stepsis\_\{i\}as a triple of sets\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)\. A stepsis\_\{i\}is considered valid if there exists an explanation such that:

Γi∪Σi⊢𝒯iai\\Gamma\_\{i\}\\cup\\Sigma\_\{i\}\\vdash\_\{\\mathcal\{T\}\_\{i\}\}a\_\{i\}\(1\)where⊢\\vdashdenotes rigorous informal entailment\. The components reflect how mathematical justifications are sourced:

- •Local Context \(Γi\\Gamma\_\{i\}\):This contains finitely many statements \(theorems, definitions, and hypotheses\) directly originating fromSS\. These statements may be explicit or implicit, but they must be effective within the current scope \(e\.g\., local assumptions within a case analysis block expire once the block concludes\)\.
- •Global Knowledge \(Σi\\Sigma\_\{i\}\):This comprises non\-trivial statements drawn from external literature or established domain consensus \(i\.e\., outside ofSS\)\. To prevent the hallucination of non\-existent theorems, any statement invoked fromΣi\\Sigma\_\{i\}must be critically examined\.
- •Background Theory \(𝒯i\\mathcal\{T\}\_\{i\}\):This comprises trivial statements, fundamental logical axioms \(e\.g\., Modus Ponens\), and rewrite rules\. By isolating𝒯i\\mathcal\{T\}\_\{i\}, we bypass the need for rigid algebraic hierarchies \(like those inMathlib\), allowing the direct manipulation of sound statements over concrete objects while safely decoupling structural type constraints from the core deductive logic\.

Crucially, an explanation\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)should not be viewed as the complete set of all contextually valid truths, but exclusively as theminimal required setof statements necessary to validate the natural language proof step rigorously\. A comprehensive discussion of this framework and what constitutes a valid explanation is provided in Appendix B\.

### 3\.2State\-Driven Verification Agent

While the tripartite framework intrinsically describes human mathematical validation, it also serves as an ideal analytical scaffolding for AI systems\. To explore the feasibility of highly efficient natural language proof verification, we implement a lightweight, state\-driven agent\. The agent utilizes this framework because it conveniently enforces traceable reasoning and provides a systematic taxonomy for isolating failure modes\.

The agent operates without relying on a formal proof assistant or domain\-specific theorem whitelists\. Instead, it maintains a discrete cognitive stateci∈\{OPEN,VERIFIED,FLAWED\}c\_\{i\}\\in\\\{\\texttt\{OPEN\},\\texttt\{VERIFIED\},\\texttt\{FLAWED\}\\\}for each stepsis\_\{i\}\.

#### Initialization and Iteration

Upon initialization, the agent assigns anOPENstatus to all deduction steps\. During each iteration, the agent selects the most criticalOPENstep and attempts to write a thick elaborationsi′s\_\{i\}^\{\\prime\}, explicitly extracting the corresponding\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)\.

#### State Transition Rules

The agent’s transitions are governed by strict auditing mechanisms to prevent both pedantic false positives and dangerous false negatives:

1. 1\.OPEN→VERIFIED\\texttt\{OPEN\}\\rightarrow\\texttt\{VERIFIED\}: A step transitions toVERIFIEDif and only if its written elaboration is logically closedandevery external item used inΣi\\Sigma\_\{i\}is explicitly supported \(either by a direct sub\-proof generated within the step file or by a precise literature citation\)\.
2. 2\.OPEN→FLAWED\\texttt\{OPEN\}\\rightarrow\\texttt\{FLAWED\}: A step is markedFLAWEDonly when the agent can exhibit anexplicit flaw witness\. This includes an exact false statement, an invalid inference from written premises, an explicit contradiction with the already verified local contextΓi\\Gamma\_\{i\}, or a demonstrably misapplied external theorem inΣi\\Sigma\_\{i\}\.
3. 3\.Flaw Confirmation\(FLAWED→OPEN\\texttt\{FLAWED\}\\rightarrow\\texttt\{OPEN\}\): To rigorously guard against pedantic false positives, any preliminary transition toFLAWEDtriggers an adversarial investigation\. The agent evaluates whether the proposed flaw witness represents a genuine structural mathematical error or merely a superficial textual nitpick \(e\.g\., relying on an unstated standard domain convention or a terminology\-dependent edge case\)\. If the perceived flaw is determined to be an epistemic ambiguity rather than a logical breakdown, the step is conservatively reverted toOPEN\.
4. 4\.Dynamic Decomposition\(OPEN→\{OPENa,OPENb\}\\texttt\{OPEN\}\\rightarrow\\\{\\texttt\{OPEN\}\_\{a\},\\texttt\{OPEN\}\_\{b\}\\\}\): If a deduction stepsis\_\{i\}is deemed too coarse or encompasses multiple non\-trivial logical leaps, the agent is permitted to dynamically decompose it into finer\-grained sub\-steps\. The originalsis\_\{i\}is replaced in the global sequence by these new sub\-steps, which are individually initialized asOPENand evaluated independently\.

We emphasize a critical design choice:failure to close a difficult theorem does not by itself count as a flaw\.If an external burden remains unsupported, the step conservatively remainsOPEN\.

#### Global Halting Criteria

The autonomous verification loop progressively updates the step states and their dependencies\. The process iterates until one of the following strict halting criteria is triggered, determining the final validity of the global proofSS:

- •Acceptance \(Soundness\):The global proof is deemed valid and accepted if and only if the entire sequence successfully reaches the terminal verified state:∀i,ci=VERIFIED\\forall i,c\_\{i\}=\\texttt\{VERIFIED\}\. If the text contains several proofs, it is considered valid if entire sequence of one of the proofs is valid\.
- •Rejection via Flaw Confirmation:If any step enters theFLAWEDstate, it must undergo the aforementioned Flaw Confirmation investigation\. If a flaw is explicitly confirmed \(i\.e\., it is verified as a genuine structural error and not reverted toOPEN\), the system halts and the global proof is immediately rejected\.
- •Rejection via Exhaustion:The agent may fail to give a disproof of a flawed step\. Thus to prevent looping on intractable gaps or missing foundational knowledge, the runner monitors observed progress signals\. If five consecutive resume iterations produce neither anOPEN→\\rightarrowVERIFIEDtransition nor anOPEN\-step split, the system terminates the loop and conservatively rejects the proof\.

#### External Knowledge Retrieval

In our pipeline, the external knowledge setΣi\\Sigma\_\{i\}is primarily sourced through active internet retrieval\. To ensure the reliability of this external knowledge, our prompt files explicitly direct the agent to prioritize established mathematical textbooks and directly relevant research literature\. While these instructions guide the agent’s search behavior, we do not computationally enforce strict constraints on the exact provenance or syntactic precision of the cited theorems\. However, general open\-ended retrieval introduces a broader theoretical challenge: unconstrained agents often overlook the strict technical constraints or local assumptions required by retrieved theorems\. This risks creating a “contextual misapplication,” where a globally valid theorem is incorrectly applied to a local context \(Γi\\Gamma\_\{i\}\) because its underlying prerequisites are not fully met\. Specifically, without the strict faithfulness constraints enforced by our framework, an agent might invoke unmentioned external knowledge to artificially justify flawed steps during extended multi\-turn executions\. Successfully navigating this latent risk underscores the critical necessity of our framework’s strict adherence to the original text\. Consequently, a crucial direction for future mathematical agents is the development of rigorous controls over external knowledge integration\. Future systems must move beyond basic search by explicitly verifying the authoritative provenance of the literature and ensuring the complete, precise extraction of all prerequisite conditions before any external theorem is applied\.

#### Structured Auditing via the Theorem Ledger

To rigorously ground external mathematical dependencies \(Σi\\Sigma\_\{i\}\), our framework asks the agent to maintain aTheorem Ledger—a centralized registry tracking external claims invoked by the agent\. During the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)tuple extraction \(full schema in Appendix\), the ledger records theStatusof cited theoremsΣj∈Σi\\Sigma\_\{j\}\\in\\Sigma\_\{i\}\. A deduction is markedVERIFIEDonly if the agent provides explicit support \(a proof sketch or precise citation\) and confirms its valid applicability within the local contextΓi\\Gamma\_\{i\}\. If any dependency remainsOPEN, downstream reasoning is flagged asconditionally closed, preventing premature validation based on unvetted assumptions\. This tracking mechanism transforms verification from a black\-box judgment into a transparent, auditable process\.

## 4Experiments

We design our empirical evaluation to answer two core research questions: \(1\) How does our structured, agentic approach compare against standard global evaluators and naive granular prompting across diverse mathematical fallacies? \(2\) How does the agent utilize its state\-driven logic to navigate and resolve highly adversarial, research\-level proofs during extended inference?

To address these, we first present a comprehensive evaluation across different verification pipelines on a curated 21\-proof suite \(Section 4\.1 and 4\.2\)\. Subsequently, we provide a deep qualitative analysis of the agent’s cognitive trajectory on specific intractable cases \(Section 4\.3\)\.

### 4\.1Experimental Setup

Diagnostic SuiteWe evaluate our framework on a highly curated diagnostic suite of 21 research\-grade mathematical proofs derived from the FirstProof challenge\[[1](https://arxiv.org/html/2606.10799#bib.bib1),[10](https://arxiv.org/html/2606.10799#bib.bib7)\]\. This suite comprises both fundamentally valid proofs \(which may contain minor, fixable omissions\) and invalid proofs containing fatal mathematical flaws or gaps\. Specifically, we structure the diagnostic suite into two distinct subsets based on their ground\-truth validity:

Valid Proofs \(11 cases\)This subset consists of 9 proofs generated by the Aletheia framework\[[8](https://arxiv.org/html/2606.10799#bib.bib6)\]and 2 proofs from OpenAI\. The Aletheia subset \(comprising variants 2A, 2B, 5A, 7B, 8B, 9A, 9B, 10A, and 10B, where the suffixes denote outputs from two distinct agent architectures\) was rigorously vetted and certified as mathematically sound by human domain experts in the original Aletheia study\. The remaining two valid cases are OpenAI’s proofs for problems 4 and 6, which have reached a definitive consensus of correctness within the formal mathematics community \(e\.g\., Zulip expert discussions\)\.

Invalid Proofs \(10 cases\)To systematically source authentic, AI\-generated flawed proofs, we analyzed the human expert critiques provided in the original FirstProof paper\[[1](https://arxiv.org/html/2606.10799#bib.bib1)\]\. We specifically targeted problems where the baseline LLMs were explicitly evaluated as committing unambiguous logical breakdowns, retrieving the corresponding raw proof texts directly from the official FirstProof repository\. There are 8 proofs collected in this way\. To ensure the inclusion of deeply adversarial examples, we augmented this set with Aletheia’s proof 7A and OpenAI’s proof 2, both of which are recognized flawed\. In particular, some of the key mathematical source material for our analysis of the FirstProof Question 7 and Question 8 cases is documented in the official solutions/comments document and in the associated mathematical background references\[[10](https://arxiv.org/html/2606.10799#bib.bib7),[22](https://arxiv.org/html/2606.10799#bib.bib9),[11](https://arxiv.org/html/2606.10799#bib.bib10),[2](https://arxiv.org/html/2606.10799#bib.bib11)\]\.

Baselines and Pipeline ConfigurationsTo isolate the source of our framework’s performance, we compare our agent against three distinct baselines, testing the limits of direct prompting and textual granularity:

1. 1\.Global GPT\-5\.4\-xhigh:A standard zero\-shot LLM\-as\-a\-judge prompt, representing the state\-of\-the\-art capability of a generic frontier model directly evaluating the monolithic text\.
2. 2\.Global Codex 5\.4\-xhigh:The identical base model used by our agent, prompted to globally verify the proof by reading sentence by sentence\. Also it is told to be strict\. This isolates the model capacity of retrieving flaws and gaps\.
3. 3\.Codex 5\.4\-xhigh Sentence\-by\-Sentence \(Ablation\):To determine whether performance gains merely stem from granular reading, we implement a baseline where the proof is mechanically split into single sentences\. The model evaluates each sentence sequentially but lacks our explicit\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)constraints and state\-driven memory\. The prompts are designed to be almost the same, except it does not have a strict constructive framework for dependencies and theorems\.
4. 4\.Constructive Verification Agent \(Ours\):The fully equipped state\-machine agent operating under the tripartite explanation framework\.

To ensure a fair comparison, the zero\-shot baseline prompt was empirically optimized through preliminary experiments to faithfully elicit the model’s peak reasoning capability\. Quantitative results for suboptimal prompt variants are omitted for brevity\.

Evaluation MetricsA verification attempt is considered successful if and only if it satisfies a strict dual\-criterion: it must accurately assign the correct global verdict \(VERIFIEDorFLAWED\),andfor flawed proofs, it must correctly isolate an offending step without hallucinating false negatives elsewhere in the proof\.

Data Contamination Risk and Audit ProtocolSince our diagnostic suite is derived from the public FirstProof challenge, data contamination remains a serious concern when evaluating frontier models\. For completed runs, we audited the retrieval and reasoning logs; if a log mentioned FirstProof\-related terms or otherwise indicated direct exposure to FirstProof source material or discussions, we discarded that run and repeated the experiment\. Apart from such explicit exposure, the risk is substantially mitigated by the structure of the protocol: a verdict is not accepted merely because the model recognizes a global answer pattern, but must be supported by local step elaborations, explicit dependency tracking, and auditable uses of external knowledge\. As an additional sanity check, we found that prompting Gemini 3\.1 Pro to “find any flaws or nontrivial gaps” rather than asking whether a proof is correct can solve all 21 cases in our suite\. We do not interpret this as evidence that a one\-shot prompt is superior to our method\. A more plausible concern is that Gemini may have been tuned, directly or indirectly, on internet\-visible FirstProof materials, creating a risk of benchmark leakage\. In particular, when Gemini judges that a correct solution route is valid, it may be recognizing an internet\-exposed answer pattern without fully attending to the subtle technical assumptions that make the argument sound\. This observation reinforces the need to treat public benchmark results for natural\-language proof verification with caution, and motivates our emphasis on auditable step\-level reasoning rather than opaque global verdicts\.

### 4\.2General Verification Performance

We evaluated the four pipelines on the 21\-proof diagnostic suite over 3 independent trials\. While the standard direct prompt baseline \(operating at a sampling temperature of 1\.0\) exhibited slight outcome variance, ours framework demonstrated macro\-level consistency, yielding identical final verdicts across all runs\. The aggregated results are presented in Table 1\.

Table 1:Verification performance on the 21\-proof diagnostic suite \(avg@3 over three independent trials\)\. We report the number of correctly classified proofs and the specific error types \(False Positives/Negatives\)\. The agent significantly outperforms the global baseline by systematically reducing hallucinated validations\.PipelineValid Proofs \(11 total\)Invalid Proofs \(10 total\)Overall Acc\.Correct \(✓\)False PositivesCorrect \(✓\)False NegativesGlobal GPT\-5\.48\.332\.677\.672\.3316/21Global Codex\-5\.47\.333\.678215\.33/21Codex 5\.4 Sentence\-by\-Sentence929118/21Agent \(Ours\)8310018/21This consistency reveals that the failures of standard LLMs in mathematical verification are not artifacts of sampling noise, but stem from systemic deductive deficiencies\.

#### Baseline Performance and Failure Modes

The baseline models—Global GPT\-5\.4, Global Codex 5\.4, and the Sentence\-by\-Sentence ablation—demonstrated severe systemic vulnerabilities, consistently failing on both valid and invalid proofs across all trials\.

- •False Negatives \(Accepting Invalid Proofs\):The baselines entirely failed to detect embedded flawed statements\. For instance, all three baseline pipelines confidently and repeatedly verified invalid proofs such as\[Aletheia 7A\]\. Without a rigorous mechanism to audit external theorems, these models were systematically deceived by formally rigorous but mathematically vacuous text\.
- •False Positives \(Rejecting Valid Proofs\):Conversely, on the 11 valid proofs, the baselines generated pedantic false positives\. They systematically flagged valid proofs such as\[Aletheia 7B, 8B, 9A\]asFLAWED, hallucinating non\-existent logical gaps or consistently complaining about standard, unstated notational conventions regardless of the sampling randomness\.

#### Agent Performance

In stark contrast, our Constructive Verification Agent achieved robust structural isolation, significantly outperforming all baselines while completely taming the inherent stochasticity of the high\-temperature setting\.

- •Reducing False Negatives:On the 10 invalid proofs, the agent successfully identified and isolated the fatal deductive flaw in 100% of the cases\. By strictly enforcing the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)constraints, the agent inherently blocked the mathematically invalid steps that bypassed the baseline evaluators\.
- •Robustness against False Positives:On the 11 valid proofs, the agent correctly verified8proofs\. For the remaining3valid proofs \(Aletheia 7B, 10A, 10B\), the agent halted in theFLAWEDorOPENstate due to genuinely ambiguous, unstated domain conventions\. The agent flagged the proof of problem 10 as flawed because it strictly adhered to the mathematical definition of the stated positive semi\-definite condition—which permits zero diagonal entries and invalidates direct element\-wise inversion—without adopting the human expert’s unstated practical convention that typical RKHS kernels inherently possess strictly positive diagonals\. Crucially, owing to its explicit Flaw Confirmation mechanism, the agent producedzeroarbitraryFLAWEDjudgments on fundamentally sound proofs\.

When provided with the 7B model’s reference solution and the initial problem conditions, our verifier successfully validated the proof \(see Appendix C\)\.

## 5Limitations and Future Works

While our framework demonstrates the immense potential of LLM\-based agents in verifying natural language mathematical proofs, certain limitations provide clear avenues for future research\.

Implicit Conventions and Human\-in\-the\-loopFirst, base LLMs inherently struggle with unstated mathematical folklore, frequently mischaracterizing benign domain\-specific notations as explicit flaws\. To address this, a highly promising direction is a human\-in\-the\-loop \(HITL\) collaborative paradigm, where the agent autonomously prunes logical dependencies but dynamically queries human experts when confronting profound epistemic ambiguities\.

Residual Hallucinations vs\. Formal GuaranteesSecond, unlike formal theorem provers that offer absolute mechanical guarantees, our purely text\-based agent remains susceptible to subtle hallucinations\. These can happen when the agent overly simplifies the application of complex, web\-retrieved external theorems\. While our current system mitigates this by enforcing strict\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)constructive elaborations, it does not currently employ a secondary adversarial pass to actively hunt for flaws within its own accepted deductions\. Future work will introduce an iterative, adversarial re\-verification mechanism to critically audit steps that have already transitioned to theVERIFIEDstate, further minimizing false negatives\.

Large\-scale EvaluationFinally, while our curated 21\-proof diagnostic suite enables deep, qualitative dissection of the agent’s cognitive trajectory and failure modes, scaling this evaluation to a massive, multi\-domain benchmark of formal and informal mathematics remains an important next step to fully chart the generalization bounds of our architecture\.

In conclusion, pure natural language mathematical agents are poised to drive continued breakthroughs in the near future\. Our work demonstrates a fundamental cognitive parallel: much like human mathematicians, autonomous agents can significantly elevate their ability to discern valid mathematical reasoning from flawed logic simply through the rigorous act of detailed elaboration\. Ultimately, our contribution extends beyond a standalone verifier implementation\.More crucially, we present a generalizable verification paradigm that can be seamlessly integrated into the internal reasoning processes of any future natural language mathematical agent\.

## References

- \[1\]M\. Abouzaid, A\. J\. Blumberg, M\. Hairer, J\. Kileel, T\. G\. Kolda, P\. D\. Nelson, D\. Spielman, N\. Srivastava, R\. Ward, S\. Weinberger, and L\. Williams\(2026\)First proof\.External Links:2602\.05192,[Link](https://arxiv.org/abs/2602.05192)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p7.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p1.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p3.1)\.
- \[2\]A\. Alfieri and C\. Novak\(2026\)Research report: some constructions in polyhedral symplectic topology suggested by ai\.External Links:2602\.13519,[Document](https://dx.doi.org/10.48550/arXiv.2602.13519),[Link](https://arxiv.org/abs/2602.13519)Cited by:[§F\.6](https://arxiv.org/html/2606.10799#A6.SS6.p3.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p3.1)\.
- \[3\]Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. Avigad\(2023\)ProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.External Links:2302\.12433,[Document](https://dx.doi.org/10.48550/arXiv.2302.12433),[Link](https://arxiv.org/abs/2302.12433)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1)\.
- \[4\]K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. Schulman\(2021\)Training verifiers to solve math word problems\.External Links:2110\.14168,[Document](https://dx.doi.org/10.48550/arXiv.2110.14168),[Link](https://arxiv.org/abs/2110.14168)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p4.6)\.
- \[5\]N\.G\. de Bruijn\(1994\)The mathematical vernacular, a language for mathematics with typed sets\.InSelected Papers on Automath,R\.P\. Nederpelt, J\.H\. Geuvers, and R\.C\. de Vrijer \(Eds\.\),Studies in Logic and the Foundations of Mathematics, Vol\.133,pp\. 865–935\.External Links:ISSN 0049\-237X,[Document](https://dx.doi.org/https%3A//doi.org/10.1016/S0049-237X%2808%2970231-3),[Link](https://www.sciencedirect.com/science/article/pii/S0049237X08702313)Cited by:[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px2.p1.1)\.
- \[6\]L\. de Moura and S\. Ullrich\(2021\)The lean 4 theorem prover and programming language\.InAutomated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28,pp\. 625–635\.Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1),[§3](https://arxiv.org/html/2606.10799#S3.p1.2)\.
- \[7\]DeepSeek\-AI, D\. Guo, D\. Yang, H\. Zhang, J\. Song, R\. Zhang, R\. Xu, Q\. Zhu, S\. Ma, P\. Wang, X\. Bi, X\. Zhang, X\. Yu, Y\. Wu, Z\. F\. Wu, Z\. Gou, Z\. Shao, Z\. Li, Z\. Gao, A\. Liu, B\. Xue, B\. Wang, B\. Wu, B\. Feng, C\. Lu, C\. Zhao, C\. Deng, C\. Zhang, C\. Ruan, D\. Dai, D\. Chen, D\. Ji, E\. Li, F\. Lin, F\. Dai, F\. Luo, G\. Hao, G\. Chen, G\. Li,et al\.\(2025\)DeepSeek\-R1: incentivizing reasoning capability in LLMs via reinforcement learning\.External Links:2501\.12948,[Document](https://dx.doi.org/10.48550/arXiv.2501.12948),[Link](https://arxiv.org/abs/2501.12948)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p1.1)\.
- \[8\]T\. Feng, J\. Jung, S\. Kim, C\. Pagano, S\. Gukov, C\. Tsai, D\. Woodruff, A\. Javanmard, A\. Mokhtari, D\. Hwang,et al\.\(2026\)Aletheia tackles firstproof autonomously\.arXiv preprint arXiv:2602\.21201\.Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p1.1),[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p2.1)\.
- \[9\]First Proof Project\(2026\)First batch \| first proof project\.Note:Project page for the first batch of First Proof problemsExternal Links:[Link](https://1stproof.org/first-batch.html)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p7.1)\.
- \[10\]First Proof Project\(2026\)First proof solutions and comments\.Note:Official solutions and commentary PDF for the First Proof projectExternal Links:[Link](https://1stproof.org/documents/FirstProofSolutionsComments.pdf)Cited by:[§F\.6](https://arxiv.org/html/2606.10799#A6.SS6.p3.1),[§1](https://arxiv.org/html/2606.10799#S1.p10.1),[§1](https://arxiv.org/html/2606.10799#S1.p7.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p1.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p3.1)\.
- \[11\]J\. Fowler\(2012\)Finiteness properties for some rational Poincaré duality groups\.Illinois Journal of Mathematics56\(2\),pp\. 281–299\.External Links:[Document](https://dx.doi.org/10.1215/ijm/1385129948),[Link](https://doi.org/10.1215/ijm/1385129948)Cited by:[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p3.1)\.
- \[12\]M\. Ganesalingam\(2013\)The language of mathematics\.InThe Language of Mathematics: A Linguistic and Philosophical Investigation,pp\. 17–38\.Cited by:[§3\.1](https://arxiv.org/html/2606.10799#S3.SS1.p2.1)\.
- \[13\]A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample\(2022\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.External Links:2210\.12283,[Document](https://dx.doi.org/10.48550/arXiv.2210.12283),[Link](https://arxiv.org/abs/2210.12283)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1)\.
- \[14\]H\. Ju, G\. Gao, J\. Jiang, B\. Wu, Z\. Sun, L\. Chen, Y\. Wang, Y\. Wang, Z\. Wang, W\. He,et al\.\(2026\)Automated conjecture resolution with formal verification\.arXiv preprint arXiv:2604\.03789\.Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p1.1),[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1)\.
- \[15\]H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe\(2023\)Let’s verify step by step\.arXiv preprint arXiv:2305\.20050\.Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p4.6)\.
- \[16\]J\. Liu, R\. Hu, and S\. Qin\(2026\)Boundedness of total cartier indices for rational singularities in families\.arXiv preprint arXiv:2605\.22782\.External Links:2605\.22782,[Link](https://arxiv.org/abs/2605.22782)Cited by:[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1)\.
- \[17\]J\. Liu and S\. Qin\(2026\)Shokurov’s global index conjecture for threefold foliations\.arXiv preprint arXiv:2605\.22735\.External Links:2605\.22735,[Link](https://arxiv.org/abs/2605.22735)Cited by:[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1)\.
- \[18\]J\. Liu, Z\. Sun, and J\. Jiang\(2026\)Optimal bounds in bend\-and\-break for foliations\.arXiv preprint arXiv:2605\.20754\.External Links:2605\.20754,[Link](https://arxiv.org/abs/2605.20754)Cited by:[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1)\.
- \[19\]D\. W\. Morris\(2015\)Introduction to arithmetic groups\.Vol\.2,Deductive Press Lieu de publication inconnu\.Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p10.1)\.
- \[20\]OpenAI\(2026\)Planar point sets with many unit distances\.Note:https://cdn\.openai\.com/pdf/74c24085\-19b0\-4534\-9c90\-465b8e29ad73/unit\-distance\-proof\.pdfCited by:[§2](https://arxiv.org/html/2606.10799#S2.SS0.SSS0.Px1.p1.1)\.
- \[21\]The mathlib Community\(2019\)The Lean mathematical library\.External Links:1910\.09336,[Document](https://dx.doi.org/10.48550/arXiv.1910.09336),[Link](https://arxiv.org/abs/1910.09336)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1),[§3](https://arxiv.org/html/2606.10799#S3.p1.2)\.
- \[22\]S\. Weinberger\(2022\)Variations on a theme of borel: an essay on the role of the fundamental group in rigidity\.Cambridge University Press\.External Links:[Document](https://dx.doi.org/10.1017/9781316529645),[Link](https://doi.org/10.1017/9781316529645)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p10.1),[§4\.1](https://arxiv.org/html/2606.10799#S4.SS1.p3.1)\.
- \[23\]Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy\(2022\)Autoformalization with large language models\.External Links:2205\.12615,[Document](https://dx.doi.org/10.48550/arXiv.2205.12615),[Link](https://arxiv.org/abs/2205.12615)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1)\.
- \[24\]K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.External Links:2306\.15626,[Document](https://dx.doi.org/10.48550/arXiv.2306.15626),[Link](https://arxiv.org/abs/2306.15626)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1)\.
- \[25\]K\. Zheng, J\. M\. Han, and S\. Polu\(2021\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.External Links:2109\.00110,[Document](https://dx.doi.org/10.48550/arXiv.2109.00110),[Link](https://arxiv.org/abs/2109.00110)Cited by:[§1](https://arxiv.org/html/2606.10799#S1.p2.1)\.

## Appendix APrompts for the Verification Agent

In this appendix, we present the prompts used to drive our state\-based verification agent\. The prompts are administered to the Codex agent as fixed instruction prompts\.

### A\.1Instruction Prompts

Prompt 1: InitializationRun a fully automatic verifier in this folder\. Read only README\.md, STEP\_TEMPLATE\.txt, OUTPUT\_FORMATS\.txt, and source/input\.txt\.Split the proof into minimal logical deduction units\. Every original source sentence with mathematical content must appear verbatim in the Original step field of at least one step file\. Initialize steps/\. Repeatedly work on the most critical untouched step, otherwise the most critical open step\.Each step file must be a thick elaboration organized by\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\), with the full original step, the exact target assertion, a detailed deduction, and a diagnosis\. Treat every step as requiring its own local closure analysis: never mark a step VERIFIED without individually checking its own writtenΓi\\Gamma\_\{i\},Σi\\Sigma\_\{i\},𝒯i\\mathcal\{T\}\_\{i\}, Deduction, and every used item ofΣi\\Sigma\_\{i\}\.For every used item ofΣi\\Sigma\_\{i\}, write the exact as\-used statement and include either a proof or a precise source, plus a brief applicability note\. Be conservative: if a used item ofΣi\\Sigma\_\{i\}is not closed by direct local reasoning, or by a proof or precise source that you can state concretely in the step file, keep it OPEN rather than VERIFIED\. Do not treat a statement as ‘confirmed’ merely because it looks standard or plausible\.A step is VERIFIED only if every used item ofΣi\\Sigma\_\{i\}is ‘confirmed’; otherwise it is OPEN, unless there is an explicit flaw witness, in which case it is FLAWED\. Initialize the verifier now: split the proof into detailed minimal proof\-obligation steps, splitting explicit intermediate assertions before downstream consequences\. Maintain only steps/, dependency\.txt, stepsprocess\.txt, and answer\.txt\. Stop only when every step has been judged as VERIFIED, OPEN, or FLAWED\.

Prompt 2: ResumeResume the verifier in this folder\. Read README\.md, STEP\_TEMPLATE\.txt, OUTPUT\_FORMATS\.txt, dependency\.txt, stepsprocess\.txt, answer\.txt, and all unresolved files in steps/\.If there is a step that is too coarse, resplit the unresolved file that is still too coarse to be one minimal logical deduction unit\. Every original source sentence with mathematical content must appear verbatim in the Original step field of at least one step file\. Then continue the main loop\.If a step has remained OPEN since the first pass and still resists closure, consider whether it has an explicit flaw witness and should be FLAWED\. For any current OPEN step hard to resolve, consult the local reference/\* materials or search online for relevant detailed information, exact statements, or precise sources\. \*If search online, you should only look for standard text book or references that DIRECTLY CONNECT to the specific problem\. DO NOT accept randomly retrieved papers merely to force a proof to work\.\*Before changing any unresolved step to VERIFIED, recheck that every used item ofΣi\\Sigma\_\{i\}has an exact as\-used statement together with either a proof or a precise source\. Do not mark a step VERIFIED by replacing the original inference with a different proof or alternative argument\. Default negative verdict is OPEN\. Use FLAWED only with an explicit flaw witness\.

Prompt 3: Flaw ConfirmInvestigate whether the FLAWED step in this folder is actually FLAWED\. Read README\.md, STEP\_TEMPLATE\.txt, OUTPUT\_FORMATS\.txt, dependency\.txt, stepsprocess\.txt, answer\.txt, the unresolved files in steps/, and reference/\* if present\.Choose exactly one currently FLAWED step, preferably the most critical one\. Keep the Original step verbatim and keep the same final assertion\. First investigate the step: expand the relevant concepts, exact statements, hypotheses, scope, and nearby lemmas in the local reference/\* materials and online source, and use this to judge whether the recorded flaw witness shows that the original sentence or exact as\-used inference is false or invalid as written\.Do not treat a mere wording, naming, or terminology imprecision as a flaw witness unless it changes the mathematical claim, breaks the local inference, or materially threatens the validity of the proof\.If yes, keep FLAWED\. If not, change it to OPEN and explain exactly why the witness fails\.

### A\.2File Formats and Step Templates

To enforce strict state tracking and prevent the LLM from generating unstructured text, the agent is required to output its intermediate reasoning and global status into highly constrained text files\. The formats for these ledgers and templates are defined below\.

Prompt 4: Global Ledgers \(OUTPUT\_FORMATS\.txt\)\[dependency\.txt\] List only external statements that are still OPEN or already FALSE\.Format: D1 \- step\(s\): \- exact as\-used statement: \- status: OPEN / FALSE \- why: \- offending point if false:\[stepsprocess\.txt\] For each step:Step: \- status: UNTOUCHED / OPEN / VERIFIED / FLAWED \- minimal unit: yes / no \- criticality: \- main blocker: \- all used sigma closed: yes / no \- flaw witness: \- next action:\[answer\.txt\] Format: Overall verdict: RUNNING / VERIFIED / FLAWEDCurrent key step:If FLAWED: \- offending step: \- exact false statement or invalid inference: \- flaw witness:If still running: \- remaining open steps: \- active dependencies:Per\-step summary: \- step: \- status: \- one\-line reason:Rule: Do not use FLAWED unless an explicit flaw witness has been written\. Do not use VERIFIED unless all used external statements are marked ‘confirmed’\.

Prompt 5: Logical Unit Template \(STEP\_TEMPLATE\.txt\)Step ID:Why this is one minimal logical deduction unit:Original step: \[paste the full original step string verbatim\]Target assertionaia\_\{i\}:Original route:Explanation: \[write a thick natural\-language elaboration that preserves the same assertion and route\]Statement Extraction\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\):Assertion:Local ContextΓi\\Gamma\_\{i\}: \-γ1\\gamma\_\{1\}: \-γ2\\gamma\_\{2\}:Global KnowledgeΣi\\Sigma\_\{i\}: \-σ1\\sigma\_\{1\}: exact as\-used statement: proof or precise source: why it applies here: status: confirmed / OPEN / false \-σ2\\sigma\_\{2\}:Sigma Support: \[for each usedσj\\sigma\_\{j\}, include either a proof or a precise source\]Background Theory𝒯i\\mathcal\{T\}\_\{i\}: \-t1t\_\{1\}: \-t2t\_\{2\}:Deduction: \[derive the assertion fromΓi\\Gamma\_\{i\}, confirmedΣi\\Sigma\_\{i\}, and𝒯i\\mathcal\{T\}\_\{i\}; if some usedσj\\sigma\_\{j\}is still OPEN, state that the route is only conditionally closed\]Diagnosis: \- conclusion preserved: \- route preserved: \- exact offending dependence, if any: \- flaw witness, if any:Step Result: \- status: UNTOUCHED / OPEN / VERIFIED / FLAWED \- main blocker: \- flaw witness: \- dependencies: \- last update:

## Appendix BExtended Discussion on the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)Framework and Explanation Validity

Consider a natural language proof textSSand its ordered sequence of steps \(substrings\)\(s1,s2,…,sn\)\(s\_\{1\},s\_\{2\},\\dots,s\_\{n\}\)\. Without loss of generality \(by carefully choosing the substrings for steps and using conjunction\) , we restrict that a step contains at most one new mathematical statement\. Throughout the paper, we consider assumptions and declarations both as mathematical statements\.

Letsis\_\{i\}be a deduction step ofSS\. Let the statementaia\_\{i\}be the assertion ofsis\_\{i\}\. Unlike fully formalized proofs in systems like Lean or Rocq, natural language mathematical proofs inherently omit trivial algebraic manipulations and elementary logical deductions to maintain readability\. In this paper, we do not require the LLM to elaborate proofs down to atomic axiomatic steps, as this would lead to an unnatural combinatorial explosion of reasoning length and degrade model performance\. When defining the assertionaia\_\{i\}extracted from a natural language proof, we adopt a stance of foundational agnosticism\. Modern informal mathematics—ranging from elementary calculus to advanced subjects like Topos theory or Wiles’ proof of Fermat’s Last Theorem—is rarely written with a strict, singular axiomatic foundation \(e\.g\., pure ZFC\) in mind\. Therefore, we do not restrictaia\_\{i\}to a specific foundational axiomatic system\. Rather, we assume the existence of a sufficient, implicit foundational theory that is universally accepted for the specific domain of the proof\.

We must also address the validity of natural language statements that appear underspecified in isolation, such as the simple assertiona=ba=b\. In strict formal systems, an equality requires explicit type alignment \(e\.g\., verifying that both sides belong to the same algebraic structure\)\. In well\-formed \(which we may assume\) natural mathematical discourse, however, such type constraints are rarely restated at every step; instead, they are implicitly inherited from the ambient context \(captured byΓi\\Gamma\_\{i\}in our framework\)\. As long as a statement is semantically well\-posed within this context, it operates as a valid deductive step\. Demanding explicit syntactic completeness for every variable introduces an unnatural overhead that misaligns with human communication\. Ultimately, if we accept a natural language proof as a valid logical artifact, we must recognize that its constituent statements—though syntactically incomplete in isolation—are rigorously well\-defined when situated in the proof’s narrative flow\. Crucially, this approach does not imply an omission of type verification\. Rather, by isolating type\-related statements, we can safely and cleanly decouple the structural type constraints from the core deductive logic, making the natural language step significantly easier to evaluate\.

For a practical way to formalize the elaboration process, we define anexplanationof the stepsis\_\{i\}as a triple of sets\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\), which encompasses all the necessary statements required to logically derive the assertionaia\_\{i\}\. Thus for any elaborationsi′s\_\{i\}^\{\\prime\}\(in natural language\), there exists a explanation\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)thatexplainsi′s\_\{i\}^\{\\prime\}\. In this context, we say the tripleexplains the elaboration if every critical mathematical assertion articulated within the natural language elaboration and the step is subsumed either directly by the sets of the triple or by the intermediate statements deduced during the derivation process\. Moreover, the derivation logically entailed by this triple must strictly adhere to the specific computational or deductive methodology dictated by the natural language text\.Γi\\Gamma\_\{i\}contains finitely many statements \(theorems, lemmas, definitions, and hypothesis\) fromSS\. The statements withinΓi\\Gamma\_\{i\}may either be explicitly stated inSSor left implicit\.Σi\\Sigma\_\{i\}comprises a finite set of statements drawn from external literature or established domain consensus, that is, outside ofSS\. Here statements fromΣi\\Sigma\_\{i\}are considered non\-trivial\. Within an explanation ofsi′s\_\{i\}^\{\\prime\}, there may exist statements fromΣi\\Sigma\_\{i\}that are implicitly assumed rather than explicitly articulated insi′s\_\{i\}^\{\\prime\}\.𝒯i\\mathcal\{T\}\_\{i\}comprises a finite set of what are often considered trivial statements \(or rewrite rules\) representing the background theory\. It assistsΓi\\Gamma\_\{i\}andΣi\\Sigma\_\{i\}in syntactically deriving the assertionaia\_\{i\}\. Fundamentally, our framework aims to model any detailed elaboration of a proof step\. Consequently, any mathematical statement invoked in such an expanded derivation must necessarily originate from this triple\.

When we say a stepsis\_\{i\}is valid, we usually mean there exists an explanation\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)ofsis\_\{i\}such that:

Γi,Σi,𝒯i⊢ai\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\\vdash a\_\{i\}Here⊢\\vdashdenotes a rigorous informal entailment\. Also, allΓi,Σi,𝒯i\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}are valid\. ForΓi\\Gamma\_\{i\}to be valid, all the statements it contains should first be effective in the stepsis\_\{i\}\. Statements inSShas their scope of effectiveness\. A context statement \(an assumption or a declaration\) has its scope: assumptions and variables are no longer valid from a certain point onwards\. Consequently,sis\_\{i\}may also fall outside the scope of other preceding mathematical statements, including lemmas and theorems\. For example, if the proof contains a case analysis, then for every case the proof establishes a block with the corresponding assumption\. The assumption’s scope terminates once the discussion for the case is over\. The theorems and lemmas proved in the case may also be invalid for the next case, if local assumptions and declarations are used\. Second, any implicit statements withinΓi\\Gamma\_\{i\}must be validly inferred from the context\. The admissibility of such implicit elements is highly sensitive to both the active discourse and the established consensus of the mathematical community\. Consequently, LLMs should be able to correctly identify valid implicit statements based on the context\. Finally, sinceΓi\\Gamma\_\{i\}contains deductions and theorems from the context, the statements ofΓi\\Gamma\_\{i\}should all be valid\. ForΣi\\Sigma\_\{i\}to be valid, all statements within it must be drawn from universally accepted mathematical facts or sound external literature\.

We now explain the validity of𝒯i\\mathcal\{T\}\_\{i\}\. Since𝒯i\\mathcal\{T\}\_\{i\}captures the routine background steps skipped by human writers, it provides a practical interface between informal mathematical text and formal axioms\. There is an immediate problem of what is considered as a nontrivial statement and has to be written explicitly\. Since the explanation here actually corresponds to expanded derivations ofsis\_\{i\}, the threshold for non\-triviality can be carefully calibrated\. Also, for𝒯i\\mathcal\{T\}\_\{i\}to be valid, all the statements it contains should be logically sound\. Throughout this framework, we operate under the standard assumption of soundness for the underlying mathematical foundation\. Let us now consider a simple example of a proof and two possible explanation of different steps\. Note that by admitting the validity of the local context in eliminating ambiguity, we can omit type declarations for the assertions and the other statements\.

Case Study: Deconstructing the Proof of2∉ℚ\\sqrt\{2\}\\notin\\mathbb\{Q\}Background Proof Context:Theorem:2\\sqrt\{2\}is an irrational number\.Step 1 \(s1s\_\{1\}\):Assume for the sake of contradiction that2\\sqrt\{2\}is a rational number\.Step 2 \(s2s\_\{2\}\):By the definition of rational numbers, there exist integersaaandbb\(whereb≠0b\\neq 0\) such that2=ab\\sqrt\{2\}=\\frac\{a\}\{b\}\.Step 3 \(s3s\_\{3\}\):We can further assume thataaandbbare coprime \(i\.e\., the fractionab\\frac\{a\}\{b\}is in its simplest form, sharing no common factors other than 1\)\.Step 4 \(s4s\_\{4\}\):Squaring both sides of the equation gives2=a2b22=\\frac\{a^\{2\}\}\{b^\{2\}\}\.Step 5 \(s5s\_\{5\}\):Multiplying both sides byb2b^\{2\}yields2​b2=a22b^\{2\}=a^\{2\}\.Step 6 \(s6s\_\{6\}\):Sincebbis an integer,b2b^\{2\}is an integer, making2​b22b^\{2\}an even number\. Therefore,a2a^\{2\}must be an even number\.Step 7 \(s7s\_\{7\}\):If the square of an integer is even, then the integer itself must be even\. Thus,aais an even integer\.Step 8 \(s8s\_\{8\}\):Sinceaais even, there exists an integerkksuch thata=2​ka=2k\.Step 9 \(s9s\_\{9\}\):Substitutinga=2​ka=2kinto the equation from Step 5 \(2​b2=a22b^\{2\}=a^\{2\}\) gives2​b2=\(2​k\)2=4​k22b^\{2\}=\(2k\)^\{2\}=4k^\{2\}\.Step 10 \(s10s\_\{10\}\):Dividing both sides by 2 yieldsb2=2​k2b^\{2\}=2k^\{2\}\.Step 11 \(s11s\_\{11\}\):Following the same logic as before, this implies thatb2b^\{2\}is an even number\.Step 12 \(s12s\_\{12\}\):Consequently,bbmust also be an even number\.Step 13 \(s13s\_\{13\}\):Since bothaaandbbare even numbers, they share a common factor of at least 2\.Step 14 \(s14s\_\{14\}\):This directly contradicts our assumption in Step 3 thataaandbbare coprime\.Step 15 \(s15s\_\{15\}\):Therefore, our initial assumption in Step 1 must be false, concluding that2\\sqrt\{2\}is irrational\.Step 7 \(s7s\_\{7\}\):•Assertion \(a7a\_\{7\}\):aais an even integer\.•Local Context \(Γ7\\Gamma\_\{7\}\):\{a2​is even\}∪\{a∈ℤ\}\\\{a^\{2\}\\text\{ is even\}\\\}\\cup\\\{a\\in\\mathbb\{Z\}\\\}\(Note:a∈ℤa\\in\\mathbb\{Z\}is an implicit statement\)•Global Knowledge \(Σ7\\Sigma\_\{7\}\):\{∀n∈ℤ,n2​is even⟹n​is even\}\\\{\\forall n\\in\\mathbb\{Z\},n^\{2\}\\text\{ is even\}\\implies n\\text\{ is even\}\\\}•Background Theory \(𝒯7\\mathcal\{T\}\_\{7\}\):∅\\emptyset\(Direct application of Modus Ponens\)Step 9 \(s9s\_\{9\}\):•Assertion \(a9a\_\{9\}\):2​b2=\(2​k\)2=4​k22b^\{2\}=\(2k\)^\{2\}=4k^\{2\}\.•Local Context \(Γ9\\Gamma\_\{9\}\):\{a=2​k,2​b2=a2\}\\\{a=2k,\\quad 2b^\{2\}=a^\{2\}\\\}•Global Knowledge \(Σ9\\Sigma\_\{9\}\):∅\\emptyset\(No external lemmas invoked\)•Background Theory \(𝒯9\\mathcal\{T\}\_\{9\}\):Equivalence properties of equality \(e\.g\., symmetry, transitivity, and substitution/congruence\) combined with fundamental properties of integer arithmetic \(e\.g\., commutativity, associativity, and evaluation of ground constants such as2×2=42\\times 2=4\)\.

We now analyze the benefits of not restricting𝒯i\\mathcal\{T\}\_\{i\}to rigid, hardcoded rules, primarily regarding its interface with foundational axioms\. Although we do not specify a definitive axiomatic system, our framework inherently assumes universally permitted operations like Modus Ponens\. This universal compatibility affords us considerable flexibility in formally specifying𝒯i\\mathcal\{T\}\_\{i\}\. Furthermore, the flexibility in specifying𝒯i\\mathcal\{T\}\_\{i\}drastically reduces the deductive overhead within⊢\\vdashand minimizes the total number of explicit statements required\. For example, in formal libraries like Lean’sMathlib, performing basic integer arithmetic typically necessitates instantiating deep algebraic hierarchies, such as commutative rings\. In contrast, allowing all kinds of sound statements bypasses this formal complexity, enabling the system to directly reason with sound statements overℤ\\mathbb\{Z\}\. Furthermore, since the operations within𝒯i\\mathcal\{T\}\_\{i\}are inherently routine, we can leverage this flexibility to formulate statements directly about the concrete objects, bypassing the need for explicit variable substitution\. This also mirrors human conventions in mathematical discourse: when executing elementary transformations, we naturally manipulate the expressions directly\. Consequently, the elements within𝒯9\\mathcal\{T\}\_\{9\}are concrete statements like\(2​k\)2=2​k⋅2​k\(2k\)^\{2\}=2k\\cdot 2k, rather than abstract, uninstantiated schemas such asx2=x⋅xx^\{2\}=x\\cdot x\.

Note that the explicit type declarationa2∈ℤa^\{2\}\\in\\mathbb\{Z\}is omitted fromΓ7\\Gamma\_\{7\}for the same reason we bypass redundant variable bindings\. By the ambient context, we establishesa∈ℤa\\in\\mathbb\{Z\}\. And since\{∀n∈ℤ,n2​is even⟹n​is even\}\\\{\\forall n\\in\\mathbb\{Z\},n^\{2\}\\text\{ is even\}\\implies n\\text\{ is even\}\\\}is an unambiguous well\-established statement under the current context, we don’t need to writea2∈ℤa^\{2\}\\in\\mathbb\{Z\}here\. Consequently, an explanation\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)should not be viewed as the complete set of all contextually valid truths, but exclusively as the minimal required set of statements necessary to validate the natural language proof step rigorously\.

In the example above, we directly structured an elaboration using the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)format\. In what follows, we demonstrate that given an elaborationsi′s\_\{i\}^\{\\prime\}of a proof step, we can extract its constituent statements and systematically categorize them into this triple framework\. Then, find an explanation that explainssi′s\_\{i\}^\{\\prime\}, though the explanation may not be valid\. Consider the following example from Firstproof generated by Aletheia\.

Case Study: Extraction Of StatementsProblem and Proof Sketch Problem:Suppose thatΓ\\Gammais a uniform lattice in a real semi\-simple group, and thatΓ\\Gammacontains some 2\-torsion\. Is it possible forΓ\\Gammato be the fundamental group of a compact manifold without boundary whose universal cover is acyclic over the rational numbersℚ\\mathbb\{Q\}? Proof:The generated proof constructs a logical contradiction centered around the compactly supported Lefschetz number,Lc​\(γ,X\)L\_\{c\}\(\\gamma,X\)\. The model computes this topological invariant through two divergent pathways\. Algebraically, it correctly applies Poincaré duality alongside theℚ\\mathbb\{Q\}\-acyclicity ofXXto deduce thatHc∗​\(X;ℚ\)H\_\{c\}^\{\*\}\(X;\\mathbb\{Q\}\)is concentrated exclusively in the top degree, cleanly evaluating toLc​\(γ,X\)=±1≠0L\_\{c\}\(\\gamma,X\)=\\pm 1\\neq 0\. Topologically, the model evaluates the 2\-sheeted regular coveringX→Y=X/⟨γ⟩X\\to Y=X/\\langle\\gamma\\rangleusing the transfer map, arriving at the valid relationχc​\(Y\)=12​\(χc​\(X\)\+Lc​\(γ,X\)\)\\chi\_\{c\}\(Y\)=\\frac\{1\}\{2\}\(\\chi\_\{c\}\(X\)\+L\_\{c\}\(\\gamma,X\)\)\. However, to mathematically force a contradiction, the model introduces a critical hallucination: it erroneously asserts that the compactly supported Euler characteristic is strictly multiplicative \(i\.e\.,χc​\(X\)=2​χc​\(Y\)\\chi\_\{c\}\(X\)=2\\chi\_\{c\}\(Y\)\) for infinite cell complexes\. By substituting this flawed generalization into the transfer equation, the generated proof strictly forcesLc​\(γ,X\)=0L\_\{c\}\(\\gamma,X\)=0, resulting in the false algebraic contradiction0=±10=\\pm 1\.Stepsis\_\{i\}\(Flawed\) "However, for any finitekk\-sheeted unbranched covering of locally compact ENRs with finite Betti numbers, the compactly supported Euler characteristic is strictly multiplicative\. Thus,χc​\(X\)=2​χc​\(Y\)\\chi\_\{c\}\(X\)=2\\chi\_\{c\}\(Y\)\."Explanation generated by LLM The author introduces a general rule regarding covering spaces\. They assert:“for any finitekk\-sheeted unbranched covering… the compactly supported Euler characteristic is strictly multiplicative\.”Expressed as a mathematical formula, the author is asserting that for any total spaceEEand base spaceBBconnected by akk\-sheeted covering map, the relationship is:χc​\(E\)=k⋅χc​\(B\)\\chi\_\{c\}\(E\)=k\\cdot\\chi\_\{c\}\(B\)To use this general formula, the author must establish the specific values forEE,BB, andkkbased on the geometry of the spaces in the proof\.•The Total Space \(EE\):The author is usingXX\(the universal cover of the manifoldMM\) as the total space\.•The Base Space \(BB\):The author defines the base spaceYYas the quotientX/⟨γ⟩X/\\langle\\gamma\\rangle\.•The Sheet Count \(kk\):The author establishes thatγ\\gammais a torsion element of order 2 \(γ2=id\\gamma^\{2\}=\\text\{id\}\)\. Becauseγ\\gammagenerates a strictly free action ofℤ/2​ℤ\\mathbb\{Z\}/2\\mathbb\{Z\}onXX,the projection map fromXXdown to the quotientYYis a regular covering map\.Because the group acting on it has exactly 2 elements,the number of “sheets” \(the size of the fiber over any point inYY\) is exactly 2\. Therefore,k=2k=2\.The author takes the specific parameters established in Step 2:•E→XE\\to X•B→YB\\to Y•k→2k\\to 2And substitutes them directly into the general formula from Step 1 \(χc​\(E\)=k⋅χc​\(B\)\\chi\_\{c\}\(E\)=k\\cdot\\chi\_\{c\}\(B\)\)\.This direct application of the parameters to the multiplicative rule yields the final assertion:χc​\(X\)=2​χc​\(Y\)\\chi\_\{c\}\(X\)=2\\chi\_\{c\}\(Y\)That is the entirety of the deduction for that specific step\. The author simply proves the covering is 2\-sheeted and plugsk=2k=2into their \(flawed\) multiplicative formula\.Statement Extraction\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\) Assertion \(aia\_\{i\}\):χc​\(X\)=2​χc​\(Y\)\\chi\_\{c\}\(X\)=2\\chi\_\{c\}\(Y\)\. Local Context \(Γi\\Gamma\_\{i\}\): γ1\\gamma\_\{1\}: The projectionX→YX\\rightarrow Yis a 2\-sheeted regular covering map, generated by a strictly free group action\. γ2\\gamma\_\{2\}:Hc∗​\(X;ℚ\)H\_\{c\}^\{\*\}\(X;\\mathbb\{Q\}\)andHc∗​\(Y;ℚ\)H\_\{c\}^\{\*\}\(Y;\\mathbb\{Q\}\)are finite\-dimensional\. γ3\\gamma\_\{3\}:XXis annn\-dimensional topological manifold\.YYis a topological manifold\. All of them are explicit\. Global Knowledge \(Σi\\Sigma\_\{i\}\): σ1\\sigma\_\{1\}:\[Flawed lemma\]For any finitekk\-sheeted unbranched covering of locally compact ENRs with finite Betti numbers, the compactly supported Euler characteristic is strictly multiplicative\. σ2\\sigma\_\{2\}: Every finite\-dimensional topological manifold is a locally compact ENR\. σ3\\sigma\_\{3\}: A topological manifold has finite compactly supported Betti numbers if its compactly supported rational cohomology is finite\-dimensional\. σ4\\sigma\_\{4\}: IfX→YX\\to Yis a covering map between manifolds, thendim\(Y\)=dim\(X\)\\dim\(Y\)=\\dim\(X\)\. Background Theory \(𝒯i\\mathcal\{T\}\_\{i\}\): t1t\_\{1\}: The property of ’the Euler characteristic being strictly multiplicative’ is defined by the following equation under algebraic rewrite rules:χ​\(total space\)=k⋅χ​\(base space\)\\chi\(\\text\{total space\}\)=k\\cdot\\chi\(\\text\{base space\}\), wherekkis the number of sheets of the covering\. t2t\_\{2\}: A regular covering map generated by a strictly free group action is an unbranched covering\. t3t\_\{3\}: A k\-sheeted covering is finite\.Deduction⊢\\vdash Sinceγ1\\gamma\_\{1\}establishes a covering mapX→YX\\to Yandγ3\\gamma\_\{3\}identifies both as manifolds,σ4\\sigma\_\{4\}confirms they share the same dimensionnn, which byσ2\\sigma\_\{2\}ensures both are locally compact ENRs\. Concurrently, becauseγ2\\gamma\_\{2\}confirms their compactly supported rational cohomology is finite\-dimensional,σ3\\sigma\_\{3\}guarantees both possess finite compactly supported Betti numbers\. Given thatγ1\\gamma\_\{1\}specifies the action is strictly free,t2t\_\{2\}classifies it as unbranched, and since it is a 2\-sheeted covering,t3t\_\{3\}confirms it is finitekk\-sheeted \(k=2k=2\)\. With all prerequisites of the flawed lemmaσ1\\sigma\_\{1\}met \(a finitekk\-sheeted unbranched covering of locally compact ENRs with finite Betti numbers\), we applyt1t\_\{1\}withk=2k=2to yield the final assertionaia\_\{i\}:χc​\(X\)=2​χc​\(Y\)\\chi\_\{c\}\(X\)=2\\chi\_\{c\}\(Y\)\.

The green highlighted part corresponds toσ1\\sigma\_\{1\}\. The yellow highlighted statement corresponds tot1t\_\{1\}\. The blue highlighted statement corresponds toγ1\\gamma\_\{1\}\. Notice a few things here\. First, we ignore the statements “γ\\gammagenerates a strictly free action ofℤ/2​ℤ\\mathbb\{Z\}/2\\mathbb\{Z\}onXX,” and “the group acting on it has exactly 2 elements\.” But we still consider our\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)explains the elaboration\. By definition, the explanation should contain every critical mathematical assertion articulated within the natural language text\. Thus, by considering the above two statements to be not critical \(which is reasonable\), we can simplify our\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)\. Given the inherent linguistic variations and rhetorical scaffolding present in human\-authored proofs, the extraction of critical statements from natural language inherently demands a degree of flexibility\. Second, we did not take arguments likeEEisXXinto account\. This is also for simplification\. By the same manner of the first example, we omit the detail of Modus Ponen\. The generated elaboration doesn’t verify all required conditions \(for example, finite Betti number\) for the flawed theorem, thus we can fill them up in the explanation\. Though the deduction process⊢\\vdashof the explanation is sound, the statements it contains are not valid, making the explanation itself not valid\. For certain steps, the logical deduction is sufficiently explicit that it requires almost no hidden calculations, rendering the corresponding elaboration essentially deterministic in practice\.

In summary, this work seeks to analyze the rigor of natural language mathematical proofs\. We do not attempt to enforce the absolute strictness required by systems like the Mathematical Vernacular \(MV\) or formal proof assistants\. Empirically, however, we demonstrate that subtle logical errors can be successfully localized simply by writing out the proof in granular detail\. The critical factor in this approach is maintaining strict faithfulness to the author’s original intent\. Ultimately, our theoretical framework serves primarily as philosophical guidance for the agent’s reasoning, rather than a rigid requirement to perfectly instantiate every formal explanation\. As our experiments confirm, the mere act of forcing the agent to elaborate in detail intrinsically elevates its verification performance\.

## Appendix CCase Study: The Boundary of Implicit Conventions \(Aletheia 7A & 7B\)

To gain deeper insights into the agent’s cognitive trajectory, we present a detailed comparative case study on the proofsAletheia 7A\(invalid\) andAletheia 7B\(valid\)\.

The original text of7Aactually consists of two separate proofs: the first is an invalid pseudoproof containing a highly concealed, fatal error concerning “multiplicity”, while the second fundamentally relies on the first\. For GPT\-5\.4, formulating a precise disproof for this specific error is difficult, as explicit counterexamples are scarcely available via web retrieval and fall outside the model’s internal parametric knowledge\. Furthermore, within the specific scope of FirstProof Problem 7, it is an accepted academic convention to assume that semisimple Lie groups are linear—an assumption that does not strictly hold in general mathematical contexts\. Consequently, an unguided agent is highly susceptible to being distracted by this linearity assumption \(generating a false flaw witness\) or by downstream errors in the second proof\.

To stress\-test our agent’s ability to identify the true structural error, we manually truncated7Ato include only the first proof and explicitly appended the linearity condition\. Across 10 independent runs, the agent yielded one false negative \(marking the flawed step asVALIDduring initialization rather checking it carefully\) and successfully rejects the proof 9 times, marking the specific stepOPENorFLAWED\. However, a closer inspection reveals a critical logical subtlety: the agent justified itsFLAWEDverdict by pointing out that the multiplicity claim explicitly contradicted the local context\. While this contradiction genuinely exists, penalizing the step strictly on these grounds is mathematically unreasonable here, as the step resides within a proof by contradiction \(reductio ad absurdum\)—where deriving absurdities is the expected trajectory\. This highlights the profound difficulty in distinguishing between an invalid inference rule and a valid derivation of a contradiction\.

Conversely, our experiments on the fundamentally valid proofAletheia 7Bperfectly illuminate the agent’s underlying verification power and its dynamic self\-correcting capabilities\. Though the agent fail to validate the proof in the 3 runs, when we evaluated7Bby explicitly providing the linearity assumption and the reference solution sketch, the agent did not simply rubber\-stamp the text\. Instead, it exhibited a rigorous, non\-linear cognitive trajectory\.

During the verification process, the agent initially proposed two potential flaw witnesses that threatened to invalidate the proof\. In one of them, the agent’s web retrieval module returned an alternative formulation of a specific series expansion\. Detecting a difference from the retrieved literature, the agent instinctively marked the author’s step asFLAWED\. The action is then rejected by ourFlaw Confirmationmechanism\. Engaged in adversarial self\-reflection, the agent re\-evaluated the discrepancy and recognized that the mere existence of a different formalization online does not mathematically invalidate the author’s specific local derivation\. Consequently, the agent correctly dismissed its own false alarm, averting a premature false positive\.

After overriding these superficial discrepancies and conducting further targeted retrieval, the agent meticulously verified the highly non\-trivial claims regarding KO\-theory \(real topological K\-theory\) and successfully closed the proof\.

This juxtaposition offers a more grounded observation: when explicit premises are provided, the agent is capable of processing complex mathematical concepts like K\-theory\. More importantly, this iterative pattern—searching for external literature, raising potential issues, and self\-correcting—demonstrates a practical pathway for scaling test\-time compute in mathematical verification\. By allocating more inference steps to information gathering and adversarial reflection, the system can progressively resolve textual ambiguities\. However, the agent’s frequent stalling on implicit human conventions serves as a humbling reminder\. It indicates that while deductive logic and external retrieval are necessary, they are not yet sufficient to fully bridge the gap between strict formalization and the nuanced, context\-dependent nature of human mathematical communication\.

## Appendix DPrompts for the Sentence\-by\-Sentence Ablation Baseline

In this section, we present the prompts used for theSentence\-by\-Sentenceablation baseline discussed in Section 4\.1\.

Unlike our main Constructive Verification Agent, which strictly enforces the\(Γi,Σi,𝒯i\)\(\\Gamma\_\{i\},\\Sigma\_\{i\},\\mathcal\{T\}\_\{i\}\)tripartite structure and maintains an explicit external theorem ledger, this ablation baseline is designed to test the effect of mere textual granularity\. Specifically, it instructs the agent to break the proof down into sentence\-level steps but only requests a “plain naive analysis in prose” without rigid dependency tracking\. This isolates the performance gains achieved by our structured deductive constraints from the gains naturally occurring when LLMs process text at a granular level\. To ensure a fair and controlled ablation, the overall execution pipeline—including the reflection and flaw confirmation prompts—remains identical to our primary version\.

Ablation Prompt 1: InitializationRun the verifier in this folder\. Read only README\.md and source/input\.txt\. Split the proof into small steps\. Create one \.txt file in steps/ for each step\. Every original source sentence with mathematical content must appear verbatim in at least one step file\. Initialize or refresh steps/, stepsprocess\.txt, and answer\.txt\.On the first pass, do not read source/theory\.txt, source/example\.txt, source/standards\.txt, or reference/\*\.Work step by step\. In each step file, keep the original text and then write a plain naive analysis in prose of whether the step closes, what is missing, or whether there is an explicit flaw witness\. Be conservative: if the step is not convincingly closed, keep it OPEN\. Use FLAWED only with an explicit flaw witness\.Maintain only steps/, stepsprocess\.txt, and answer\.txt\. Stop only when every step has been marked VERIFIED, OPEN, or FLAWED\.

Ablation Prompt 2: ResumeResume the verifier in this folder\. Read README\.md, stepsprocess\.txt, answer\.txt, and all unresolved files in steps/\. If a step is still too coarse, split it smaller\. Every original source sentence with mathematical content must appear verbatim in at least one step file\.Continue step by step\. If a step has remained OPEN since the first pass, consider whether there is an explicit flaw witness and it should be FLAWED\. For a hard OPEN step, you may consult reference/\* or search online for relevant details\. Before changing any unresolved step to VERIFIED, recheck that the step really closes\.Default negative verdict is OPEN\. Use FLAWED only with an explicit flaw witness\. Maintain only steps/, stepsprocess\.txt, and answer\.txt\.

## Appendix EImplementation Details and Hyperparameters

To ensure full reproducibility of our empirical results, we detail the exact execution environment and API parameter configurations utilized for our framework\.

#### Execution Environment\.

All experimental evaluations were conducted within thecodexframework \(version 0\.124\.0\)\. We strictly utilized the framework’s default configuration profile for environmental setup\. Beyond this basic scaffolding, all complex agentic behaviors, formatting rules, and state\-machine constraints were injected directly into the GPT\-5\.4\-xhigh engine via natural language system prompts\. This design avoids overfitting to specialized framework configurations and explicitly demonstrates the out\-of\-the\-box generalizability of our verification approach\.

#### LLM Generation Hyperparameters\.

To maintain a rigorously fair comparison, identical generation parameters were applied to the GPT\-5\.4\-xhigh API calls across all baselines and our agentic pipeline\. We deliberately operated at a standard temperature of 1\.0 to simulate natural generation variance\. The fact that our agent yields deterministic, monotonic convergence under these high\-entropy sampling conditions further corroborates the robustness of our prompt\-driven constraints\. The complete parameter suite governing the LLM API requests is summarized in Table[2](https://arxiv.org/html/2606.10799#A5.T2)\.

Table 2:Complete hyperparameter configurations applied directly to the GPT\-5\.4\-xhigh API endpoints across all verification pipelines\.

## Appendix FA Worked Trace of a Successful Verification Run for Problem 7b

This appendix records a representative successful verification trace for Problem 7b, based on the segment of the execution log that culminates in a fully verified proof state\. The point of this example is not that the agent generated a correct proof in one shot\. Rather, the log shows a staged verification process in which the agent repeatedly refines the proof graph, isolates unresolved dependencies, revises an incorrect intermediate diagnosis, and only then closes the remaining steps\.

The successful portion of the run is the segment in which the global status eventually changes toOverall verdict: VERIFIED\. Within that segment, the agent’s behavior is best understood as a sequence of state transitions over a ledger of proof obligations, rather than as a single forward derivation\.

### F\.1Initial Reduction of the Open Proof State

At the beginning of the successful segment, the proof is not globally closed\. The agent first strengthens the verification of the real assembly injectivity step, recorded asstep\_15a\_real\_assembly\_injectivity\. The key effect of this move is structural: it eliminates one major upstream dependency and reduces the remaining unresolved part of the proof to the signature\-package portion\.

The agent then observes that the existing stepstep\_15b1\_signature\_equals\_assemblyis too coarse\. In its own diagnosis, this step mixes two logically different bridges:

1. \(i\)theassembly/index bridge, namely that the analytic symmetric signature is the assembly image of a signature class; and
2. \(ii\)thecharacteristic\-class bridge, namely that this signature class corresponds rationally to the Poincaré dual of the HirzebruchLL\-class\.

Instead of keeping this as one unresolved block, the agent explicitly resplits it into smaller units:

- •step\_15b1a\_signature\_class\_to\_assembly
- •step\_15b1b\_signature\_class\_to\_lclass
- •step\_15b1c\_signature\_equals\_assembly

It also rewires the downstream chain so that each later step depends on the newly separated obligations rather than on one monolithic unresolved assertion:

step\_15b2\_m0\_pushforward\_formula→\\rightarrowstep\_15c\_lclass\_equality→\\rightarrow step\_16\_degree\_pm1→\\rightarrowstep\_17\_final\_contradiction

This resplitting is the first decisive move in the successful run\. It turns a vague unresolved block into a small dependency graph with identifiable root causes\.

### F\.2Compression to Two Genuine External Gaps

After the split, the proof still contains severalOPENsteps, but the agent recognizes that these are largely downstream consequences of only two genuine external gaps, recorded in the dependency ledger asD6b1aandD6b1b\. Informally:

- •D6b1a:the realK​OKO\-theoretic assembly/index bridge\.
- •D6b1b:the realK​OKO\-homologicalLL\-class bridge\.

This is an important feature of the trace\. The raw number of open files is not itself the right complexity measure\. Once the proof has been resplit correctly, the open graph becomes shallow: many open steps are merely inherited consequences of a very small number of unresolved inputs\.

### F\.3An Incorrect Flaw Diagnosis and Its Retraction

The run then exhibits a nontrivial self\-correction\. The agent temporarily marksstep\_15b1c\_signature\_equals\_assemblyasFLAWED\. The reason given is a purported contradiction with a Rosenberg–Weinberger normalization theorem, which seemed to show that the exact realK​OKO\-theoretic formula written in the step could not hold with coefficient11and the HirzebruchLL\-class exactly as written\.

This is not the final diagnosis\. A separate follow\-up phase is launched specifically to determine whether the recorded flaw witness really implies that the original step is false as used\. This matters because the verification protocol distinguishes sharply between:

- •a statement that isgenuinely false;
- •a statement that may still be true, but whose current justification isincomplete or misalignedwith the cited source\.

Upon re\-reading the relevant source, the agent concludes that the previous witness targeted the signature\-operator transformationsns\_\{n\}, whereas the proof step under inspection was using a symmetric\-signature route\. Therefore the witness didnotactually refute the exact as\-used inference\. The result is a rollback fromFLAWEDtoOPEN\.

This retraction is one of the most informative parts of the trace\. It shows that the agent is not merely searching for counterexamples, but is also checking whether a counterexample hits the correct formal target\. In other words, the system distinguishes a failed proof route from a failed theorem statement\.

### F\.4Closure of the Two Remaining Root Dependencies

After retracting the incorrect flaw diagnosis, the agent returns to the two root gaps\.

#### 1\. ClosingD6b1a\.

The agent verifiesstep\_15b1a\_signature\_class\_to\_assembly\. The successful route here is to replace an indirect complex\-KK\-theoretic justification with a more exact realK​OKO\-theoretic source: Rosenberg and Weinberger’s Lipschitz\-signature theorem is used to construct the realK​OKO\-homology signature class and to identify its assembly image with the symmetric signature\. Once this step is markedVERIFIED, the remaining active dependency set shrinks from \{D6b1a,D6b1b\} to just \{D6b1b\}\.

#### 2\. ClosingD6b1b\.

The agent closes this gap by rewritingstep\_15b1b\_signature\_class\_to\_lclass\. Here the successful move is not simply to cite a missing theorem verbatim\. Instead, the agent builds a local bridge:

1. \(1\)identify the real signature class inK​OKO\-homology;
2. \(2\)complexify it to the standard complex signature class;
3. \(3\)invoke the known complexKK\-homologicalLL\-class formula;
4. \(4\)use rational real/complex comparison to recover the required realK​OKO\-homology coordinates\.

This is the step at which the open graph finally collapses\. Oncestep\_15b1b\_signature\_class\_to\_lclassis verified, the recombination stepstep\_15b1c\_signature\_equals\_assemblyalso becomes verifiable, since its two incoming components are now both closed\.

### F\.5Propagation to the Final Contradiction

After the two root dependencies are closed, the rest of the proof is discharged by dependency propagation rather than by new conceptual discoveries\.

- •step\_15b1c\_\.\.\.is verified by recombining the now\-verified assembly/index bridge with theLL\-class bridge\.
- •step\_15b2\_\.\.\.is verified by specializing the base formula toM0M\_\{0\}andX0X\_\{0\}\.
- •step\_15c\_\.\.\.is verified by using injectivity of the real assembly map to pull back the signature equality\.
- •step\_16\_\.\.\.is verified by reading off the top\-degree consequence, namely thatD=±1D=\\pm 1\.
- •step\_17\_\.\.\.is finally verified by combining this conclusion with the already verified evenness statement forDD\.

\(Note: Long file names are abbreviated here for narrative flow, while remaining rigorously tracked in the system ledgers\.\)

At that point, the global ledger is updated toremaining open steps: noneandOverall verdict: VERIFIED\. The run concludes with a consistency pass over the step files, the dependency ledger, the process summary, and the final answer file to ensure that no staleOPENorFLAWEDstatus remains\.

### F\.6Interpretation

This trace is useful because it illustrates what a successful agentic proof\-verification run actually looks like in practice\. It is not a single\-pass proof synthesis\. Instead, it has four characteristic ingredients:

1. Phase 1:State Decomposition:A coarse unresolved claim is split into minimal logical units\.
2. Phase 2:Dependency Localization:Many apparent open steps are reduced to a very small set of root gaps\.
3. Phase 3:Error Correction:An intermediateFLAWEDdiagnosis is explicitly re\-examined and retracted when the witness is found to miss the exact target statement\.
4. Phase 4:Closure by Propagation:Once the root gaps are closed, the remaining steps verify in sequence through the dependency graph\.

For this reason, the7Bexample should not be described as a case where the agent simply “found the proof\.” A more accurate description is that it executed a ledger\-guided verification procedure: it refined the proof graph, isolated the true bottlenecks, corrected a mistaken local refutation, and only then propagated the repaired information to a fully verified final contradiction\.