Step-Level Elaboration Improves Natural Language Verification of Research-Level Mathematical Proofs

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 attempts detailed constructive elaboration for each deduction step while strictly constraining the sources of applied theorems. We evaluate on a curated adversarial diagnostic suite of research-level proofs drawn from the FirstProof challenge. A systematic ablation study suggests that constructive step-level elaboration and control over external mathematical sources are indispensable for localizing subtle logical errors. Beyond improving 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 shifting verification from direct judgment to detailed constructive proof elaboration, together with control over external mathematical sources, can substantially improve pure natural-language agents' 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 implications for future automated proof-review agents.