ProofDiff: Auditable Argument-Level Comparison of AI-Generated Mathematical Proofs
Abstract: Mathematical understanding depends on the route from hypotheses to conclusion: how the parts of a proof function and which dependencies carry the argument forward. This structure can persist when wording or notation changes, while a small alteration to a hypothesis or inference can produce a different argument beneath similar prose. Formal verification can establish that a rewrite proves the same theorem, but not whether it follows the same mathematical route. Comparing informal proofs, especially those produced or revised by generative models, therefore requires reconstructing which claims, dependencies, and reasoning steps are preserved, reorganized, or replaced. We present ProofDiff, a system for comparing informal mathematical documents. It is designed to support human review, not to certify mathematical correctness. Given two documents, ProofDiff independently constructs a source-grounded argument map for each and proposes correspondences between the resulting maps. Each map captures the document's claims and reasoning steps and records the typed relations that connect them. An integrated human-review layer allows reviewers to revise the maps and correspondences while preserving an auditable history. Comparing the two argument maps provides a basis for inspecting whether the documents follow the same mathematical route and where their claims or dependencies differ. We demonstrate ProofDiff on four illustrative pairs of AI-generated proofs, ranging from a detailed proof and its concise revision to proofs using different mathematical strategies.