ProofDiff maps how AI-generated mathematical proofs differ

Comparing routes, not just answers

A mathematical proof connects assumptions to a conclusion through intermediate claims and reasoning steps. Ordinary text comparisons highlight changed words, but they do not reconstruct which claims support which inferences. Formal proof assistants address another question: whether a derivation establishes a stated theorem. Successfully checking two proofs does not, by itself, explain whether they take the same mathematical route.

ProofDiff tackles that comparison problem for informal mathematical documents. It constructs a separate argument map for each document, then proposes links between corresponding parts. Its output is evidence for review, not a verdict about mathematical correctness, originality or influence.

The work is presented in an arXiv preprint whose first version is dated 6 November 2026. The authors report that an earlier version was accepted by the NeurIPS 2026 Workshop on AI for Verifiable Coding; that acceptance should not be treated as establishing peer-review status for this exact version.

Turning documents into argument maps

An argument map is a directed graph: a collection of units, called nodes, connected by links that have a direction and a specified meaning. Nodes can represent definitions, theorems, supporting results called lemmas, proof steps or explanations. A statement and its proof occupy separate nodes.

The links distinguish mathematical support from background context. One can record that a step uses an earlier result, another that it invokes a definition’s conditions. Other links connect proofs to their statements or record contextual vocabulary without claiming that it justifies an inference.

ProofDiff accepts TeX—the source format commonly used for mathematical writing—and PDFs. When TeX is available, it takes precedence. Parsing rules identify structural blocks, after which a language model describes their mathematical content, assumptions and roles. The model can also divide a long proof into smaller steps. Each node retains references to the source passages behind it, so reviewers can inspect more than a model-written summary.

Further model calls propose and classify relationships within each document. Only after both maps have been built independently does the system propose cross-document correspondences. These can connect individual nodes or groups, accommodating a detailed argument compressed into one short passage.

An important qualification is that the current automatic matching uses node descriptions, not the maps’ connection structure. Those connections remain available for human inspection but do not enter candidate generation or scoring.

What the examples showed

The demonstration used eight short AI-generated proofs arranged into four pairs. All inputs were TeX, and all model-backed stages within ProofDiff used GPT-5.5. The reported results were automatic, without saved human edits or imported correspondences.

Across the pairs, the system produced 21 candidate correspondences. An illustrative confidence filter of 0.75 retained 12 for display. These scores are uncalibrated heuristics, not probabilities that a match is correct, and passing the filter does not constitute acceptance.

For two proofs that there are infinitely many primes, the second was generated from the first proof’s argument blueprint. All four proposed correspondences remained visible at the filter setting. A separately stated definition of a prime appeared only in the original map and remained unresolved.

Two proofs of the Cauchy–Schwarz inequality used different strategies. At the same setting, visible matches connected their shared definition and theorem statement, while method-specific lemmas and proofs remained unresolved. Similarly, proofs that the real numbers are uncountable shared visible correspondences for their countability definitions and conclusion, but not for their distinct diagonal and measure-theoretic proof machinery.

The fourth pair compared a detailed mean value theorem proof with a concise revision. A grouped correspondence connected several original argument units to one compact proof node, illustrating how the system can represent compression rather than merely matching passages one to one.

Inspectable, but not validated at scale

A browser interface places the maps side by side and exposes source evidence, proposed links and their explanations. For TeX-backed comparisons, reviewers can revise the maps and correspondences while preserving an audit history and a restorable automatic baseline.

The evidence nevertheless establishes feasibility, not general performance. The authors inspected all 21 candidates themselves, without independent evaluation. Human-written proofs, longer documents and revisions of real mathematical texts remain to be studied. The examples do not establish how many genuine correspondences the system misses or validate its display threshold.

Model-generated descriptions and links can omit structure, introduce unsupported relationships or vary between runs. Source references make those errors inspectable; they do not eliminate them. An unmatched node is therefore unresolved—not evidence of novelty. ProofDiff’s contribution is a framework for examining proposed similarities and differences while keeping human mathematical judgment essential.