Agent-Based Auditing of Mathematical Proofs in Research Papers

We present an agent-based framework for auditing mathematical proofs in theoretical computer science and machine learning research papers. Our system operates directly on informal mathematical documents and constructs a structured proof dependency graph over definitions, lemmas, and theorems. The proposed auditing pipeline performs local proof verification, global consistency analysis, and adversarial counterexample search while maintaining persistent audit artifacts across the document. The system generates structured audit reports that identify logical gaps, hidden assumptions, invalid inference steps, notation inconsistencies, and cross-lemma dependency failures. We evaluate our approach on a curated set of mathematical and ML theory papers with injected and naturally occurring proof errors, demonstrating detection performance. Our results suggest that agentic structural auditing is a promising direction for improving the reliability of machine-generated and human-written mathematical research.