ProofDiff: Auditable Argument-Level Comparison of AI-Generated Mathematical Proofs

Matan Tsafrir, Esdras Medeiros, Jorge Poco, Kevin Gomez, Eduardo V. Teixeira +1

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…