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

The paper introduces a framework for strict step-level verification of mathematical proofs using Large Language Models (LLMs), addressing limitations of global evaluation methods that suffer from context poisoning. The approach, evaluated on an adversarial suite of research-level proofs from the FirstProof challenge, demonstrates that maintaining detailed context and constraining theorem sources significantly enhances error localization and reduces logical hallucinations. This methodology not only improves proof verification but also reshapes the understanding of errors, suggesting a pathway for developing more robust automated proof-review systems.