Beyond Formal Correctness: Structure-Aware Evaluation of Informal–Formal Proof Correspondence

Proof assistants such as Lean certify that a formal proof establishes its target theorem, but do not determine whether it follows the reasoning expressed in a supplied natural-language proof. We introduce Goal–Context Delta Alignment (GCDA), a reference-conditioned framework for measuring this proof-process correspondence. GCDA recovers natural reasoning-state transitions and their derived dependencies, and traces the formal proof through Lean goal states connected by tactic-induced Goal–Context Deltas. It aligns each informal transition with a connected formal transition region, then checks required-region coverage, whole-proof coherence, and dependency direction. We evaluate GCDA on ProofRouteBench, a benchmark built from ReasBook and miniF2F with 4,888 proof variants across 670 theorem groups. GCDA achieves MacroAUCs of 0.9398 on ReasBook and 0.8788 on miniF2F, with strong separation on explicit dependency-certificate and cycle changes.