Evaluating Research-Level Math Proofs via Strict Step-Level Verification
Yifeng Sun
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.
AI Impact Assessments
(1 models)Scientific Impact Assessment
Core Contribution
This paper proposes a shift from global LLM-based proof evaluation to strict step-level verification for research-level mathematical proofs. The central idea is a tripartite framework (Γᵢ, Σᵢ, Tᵢ) that decomposes each deduction step's logical dependencies into local context, external knowledge, and background theory. Rather than asking an LLM to globally judge a proof's validity, the system forces constructive elaboration of each step, treating verification failure as evidence of a logical gap. The framework is implemented as a state-driven agentic workflow with explicit state transitions (OPEN → VERIFIED/FLAWED), a flaw confirmation mechanism, and structured halting criteria.
The key insight—that "context poisoning" in global evaluation can be mitigated by forcing granular, constrained elaboration—is conceptually sound and connects to broader themes in process-based reward modeling (Lightman et al., 2023). The reframing from anomaly detection to constructive elaboration is a meaningful conceptual contribution.
Methodological Rigor
The evaluation raises significant concerns. The diagnostic suite contains only 21 proofs, which is extremely small for drawing robust quantitative conclusions. While the author argues this enables "absolute clarity," the sample size fundamentally limits statistical power. The reported "avg@3" evaluation (3 independent trials) is minimal, and the aggregate accuracy numbers (e.g., 18/21 vs. 16/21) represent differences of 2-3 proofs—well within noise margins for such a small dataset.
The baseline comparisons are somewhat unfair. The "Global GPT-5.4" and "Global Codex-5.4" baselines use simple zero-shot prompting, while the agent uses an elaborate multi-turn workflow with internet retrieval, multiple resume iterations, and structured prompt templates. The ablation (sentence-by-sentence without tripartite constraints) is more informative but still achieves 18/21—identical to the agent's overall accuracy. The agent's advantage is concentrated entirely in zero false negatives on invalid proofs versus 1 for the ablation, a difference of a single proof.
The data contamination concern is acknowledged but inadequately addressed. The author notes that Gemini 3.1 Pro can solve all 21 cases with a simple prompt, suggesting benchmark leakage. The auditing protocol (discarding runs that mention "FirstProof-related terms") is heuristic and may not catch implicit knowledge embedded in model weights.
The claim of "macro-level consistency" (identical verdicts across runs) for the agent is interesting but not deeply analyzed—it could reflect the deterministic structure of the prompt pipeline rather than genuine robustness.
Potential Impact
The paper addresses a genuine need: as LLMs increasingly tackle mathematical reasoning, the ability to verify proofs in natural language is becoming critical. The framework could serve as a module within larger mathematical AI systems (like Aletheia or RETHLAS). The observation that remaining failures stem from "pedantic hyper-rigor" about unstated domain conventions, rather than logical hallucinations, is a genuinely useful empirical finding that could guide future system design.
However, the practical impact is limited by several factors: (1) the framework is prompt-engineering-heavy and tightly coupled to a specific model (Codex/GPT-5.4), raising portability concerns; (2) the computational cost of multi-turn agentic verification with internet retrieval is not discussed; (3) the approach lacks formal guarantees by design, occupying an awkward middle ground between informal human review and formal verification.
Timeliness & Relevance
The paper is timely, appearing alongside notable achievements in AI mathematical reasoning (OpenAI's unit distance result, Aletheia's FirstProof solutions). The focus on verification rather than generation addresses an important gap. The FirstProof benchmark provides a relevant testbed of genuine research-level mathematics.
Strengths
1. Conceptually clear framework: The tripartite (Γᵢ, Σᵢ, Tᵢ) decomposition is well-motivated and connects naturally to how mathematicians structure their reasoning.
2. Qualitative depth: The case studies (Appendices C and F) provide genuinely informative traces of the agent's behavior, including the self-correction on Problem 7B.
3. Honest failure analysis: The paper forthrightly discusses cases where the agent fails due to unstated conventions, turning these into insights about the benchmark itself.
4. Zero false negatives: Achieving no false acceptances on invalid proofs is a meaningful result for a soundness-prioritizing system.
Limitations
1. Tiny evaluation scale: 21 proofs is insufficient for reliable quantitative claims. The paper would be stronger framed as a purely qualitative/proof-of-concept study.
2. Marginal quantitative improvement: The agent achieves 18/21 overall versus 18/21 for the sentence-by-sentence ablation. The improvement is entirely in error type distribution, not aggregate accuracy.
3. Single model evaluation: All experiments use GPT-5.4/Codex variants. Generalization to other models is unknown.
4. Heavy prompt engineering: The framework relies on carefully crafted, lengthy prompt files. Robustness to prompt variation is not studied.
5. No cost analysis: The multi-turn agentic workflow with internet retrieval likely incurs substantial computational costs compared to single-pass baselines—this tradeoff is never quantified.
6. Independent researcher without peer review signal: The paper is a solo effort, and while this doesn't inherently diminish quality, the evaluation design would benefit from external methodological scrutiny.
7. Theoretical framework is descriptive rather than prescriptive: The (Γᵢ, Σᵢ, Tᵢ) formalism is presented with mathematical notation but lacks formal properties or guarantees—it serves primarily as prompt scaffolding.
Overall Assessment
This paper presents an interesting conceptual framework for step-level proof verification with some compelling qualitative insights, particularly around the taxonomy of verification failures. However, the empirical evaluation is too small-scale and the quantitative improvements too marginal to support the paper's ambitious claims. The work is best understood as an early proof-of-concept that identifies a promising direction rather than a validated methodology. The gap between the paper's rhetorical framing (paradigm shift, theoretical foundation for automated proof review) and its actual evidence base (21 proofs, marginal aggregate improvement) is notable.
Generated Jun 10, 2026
Comparison History (23)
Paper 1 addresses a concrete, actionable problem in LLM-based mathematical proof verification with a rigorous methodology (ablation studies, adversarial benchmarks) and clear practical applications for automated proof review. Paper 2, while intellectually provocative, proposes a speculative theoretical framework for AI alignment grounded in controversial methodology (training on suicide notes) that raises serious ethical concerns and lacks empirical grounding beyond surface-level linguistic pattern matching. Paper 1's contributions are more immediately useful, methodologically sound, and likely to influence follow-up research in formal verification and mathematical reasoning.
Paper 1 addresses a critical bottleneck in AI reasoning—verifying research-level mathematical proofs. By introducing a strict step-level verification framework, it mitigates 'context poisoning' and lays the foundation for automated proof-review systems. This has transformative potential for advancing AI capabilities in frontier mathematics and formal logic. While Paper 2 presents a strong theoretical framework for Theory of Mind, the saturation of ToM benchmarks limits its broader methodological impact compared to solving complex, open-ended mathematical verification.
Paper 1 likely has higher impact due to strong timeliness and broad real-world applicability: runtime governance for production AI agents addresses an urgent enterprise need and can influence security, policy, systems, and agent architecture. It proposes a clear, composable reference architecture with correctness invariants, threat coverage across workflows, and performance measurements, suggesting methodological rigor and deployability. Paper 2 is novel and valuable for LLM proof evaluation, but its immediate applications are narrower (research-proof verification), and impact may be more confined to AI-for-math/verification communities.
Paper 1 is more scientifically impactful due to a clearer, more novel methodological shift (from global to strict step-level verification) that directly targets a known failure mode (“context poisoning”) and is validated on an adversarial, research-level proof suite with ablations and failure taxonomy. It has strong real-world implications for automated proof checking and trustworthy mathematical reasoning, with potential cross-field relevance to verification, evaluation, and agent reliability. Paper 2 is timely and applicable, but co-evolving agent/environment within one LLM is less rigorously grounded and shows modest benchmark gains, with higher risk of reward hacking/self-referential bias.
Paper 2 addresses a fundamental challenge in AI reasoning—rigorous mathematical proof verification—with a novel step-level verification framework that yields actionable methodological advances. Its contributions (context poisoning identification, strict deductive constraints, failure taxonomy analysis) have broad implications for automated reasoning, formal verification, and agentic AI systems. The work is timely given rapid LLM advancement and has clear extensibility to other domains requiring logical rigor. Paper 1, while valuable for educational research, addresses a narrower audience with semantic/bibliometric analysis of construct definitions, offering more incremental conceptual clarification than methodological breakthrough.
Paper 2 introduces a novel benchmark evaluating AI agents across the research lifecycle, a highly active and critical area in AI development. Benchmarks for autonomous research agents have broader applicability and the potential to drive widespread future research compared to Paper 1's domain-specific focus on mathematical proof verification, giving Paper 2 a broader scope and higher potential scientific impact.
Paper 2 addresses a more fundamental and broadly impactful problem—rigorous step-level verification of mathematical proofs—with a novel framework that reveals deep insights about LLM reasoning failures (context poisoning, pedantic hyper-rigor). Its contributions have broader implications for automated theorem proving, formal verification, and agentic reasoning systems. The discovery that remaining errors stem from implicit domain conventions rather than logical hallucinations is a significant conceptual advance. Paper 1, while valuable for engineering education evaluation, is more application-specific and incremental in its benchmarking contribution.
Paper 1 tackles a fundamental bottleneck in AI capabilities—complex logical reasoning and mathematical proof verification. By shifting to step-level verification, it addresses core issues like hallucination and context poisoning in LLMs. This has profound implications for advancing AI's ability to independently verify and discover novel scientific knowledge. While Paper 2 offers significant practical improvements for Computer Use Agents, Paper 1's contribution to formal reasoning and foundation model evaluation presents a broader and deeper theoretical impact across AI and mathematics.
Paper 2 has higher potential impact due to strong novelty and timeliness: it tackles rigorous verification of research-level math proofs by LLMs via strict step-level constraints, addressing a widely recognized failure mode (context poisoning) in AI reasoning. Its methodology includes an adversarial benchmark, ablations, and detailed error taxonomy, supporting rigor and reproducibility (code released). Applications span automated proof checking, trustworthy AI, and formal methods, with broad cross-field relevance in ML, mathematics, and verification. Paper 1 is valuable for industrial fault diagnosis but is more incremental within a narrower application domain.
Paper 2 addresses a fundamental aspect of LLM training and alignment (self-distillation and feedback), offering deep insights into token-level advantages. This has broad, immediate implications across all domains of LLM development. Paper 1, while innovative in its step-level verification approach, is more narrowly focused on mathematical proof evaluation.