ProofDiff

ProofDiff compares two mathematical papers that prove related results. It extracts a structured argument map from each paper, discovers typed dependencies within each argument, proposes cross-paper alignments, and renders an interactive flow view for inspection and optional human curation.

TeX is the semantic source whenever it is available. PDF extraction is a fallback for papers without TeX; PDFs accompanying TeX are used only for visual evidence.

Scope and limitations

ProofDiff produces candidate correspondences, not mathematical or historical verdicts. It does not certify correctness, novelty, authorship, or influence. Confidence values are heuristic scores rather than calibrated probabilities, and an absent or filtered candidate is not proof that material is unique. Model-backed stages may produce different valid results between runs.

Requirements

• Python 3.12 or newer
• uv
• A TeX installation providing latexmk and synctex
• Internet access for model calls and for D3/KaTeX assets in generated flow pages

Install the locked environment from the repository root:

uv sync --frozen --no-editable

The non-editable installation verifies the packaged application rather than loading the source tree directly. Confirm the installation with:

uv run --no-sync proofdiff --help

The commands below use uv run --no-sync so that uv runs the locked, non-editable environment without replacing it with an editable installation.

Credentials

Set the credential required by the provider selected in src/proofdiff/models.json:

export OPENAI_API_KEY="..."
# or ANTHROPIC_API_KEY / HF_TOKEN

Credentials are read from environment variables. Never add real credentials to this repository. .env files are ignored; .env.example contains variable names only.

Paper examples

The repository includes the four example pairs used in the paper:

Pair	Directory	Comparison
Infinitude of primes	pairs/infinitude-primes-claude-gemini	Preservation under reformulation
Cauchy--Schwarz	pairs/cauchy-schwarz-discriminant-normalization	Different proof strategies
Uncountability of the real numbers	pairs/uncountability-diagonal-measure	Different proof machinery
Mean value theorem	pairs/MVT	Compression across levels of detail

The inputs were generated for the ProofDiff project through Claude, Gemini, and ChatGPT interfaces. See THIRD_PARTY_NOTICES.md for their provenance and the third-party audit.

Run one example end to end by replacing <pair-id> below:

uv run --no-sync proofdiff extract pairs/<pair-id>
uv run --no-sync proofdiff compile pairs/<pair-id>
uv run --no-sync proofdiff outline pairs/<pair-id>
uv run --no-sync proofdiff import pairs/<pair-id>
uv run --no-sync proofdiff segment pairs/<pair-id>
uv run --no-sync proofdiff enrich pairs/<pair-id> --model gpt
uv run --no-sync proofdiff align pairs/<pair-id> --model gpt
uv run --no-sync proofdiff flow pairs/<pair-id>
uv run --no-sync proofdiff validate pairs/<pair-id>

enrich performs node enrichment and typed-relation discovery by default. proofdiff relate reruns relation discovery without renaming or splitting nodes. For malformed enrichment output, enrich permits six total attempts (one initial request plus five targeted corrections) before stopping without saving the invalid section. Ordinary generated artifacts and model logs remain local and are ignored by Git; the exact paper outputs are handled separately as described below. Open the final visualization at pairs/<pair-id>/rendered_nodes/flow.html.

To serve the flow view with local curation enabled, run:

uv run --no-sync proofdiff flow-edit pairs/<pair-id>

Tests

Run the self-contained release tests with:

uv run --no-sync pytest -k "not live_hf_ping"

The included release tests use public or synthetic fixtures. Tests requiring live provider access are excluded by the command above.

Repository layout

src/proofdiff/    application source
schemas/          exported JSON schemas
tests/            self-contained tests and synthetic TeX fixtures
pairs/            the four paper examples
src/proofdiff/models.json  packaged model-provider registry
pyproject.toml    package and dependency metadata
uv.lock           locked Python environment
LICENSE           MIT License for software
LICENSE-CONTENT   CC BY 4.0 notice for non-code material
LICENSING.md      license scope and exceptions
THIRD_PARTY_NOTICES.md  example provenance and upstream notices
CITATION.cff      software and paper citation metadata

Release provenance

This clean release was derived from the internal source baseline recorded in PROVENANCE.md. The paper should cite the tagged public release and archival DOI rather than a moving branch.

Paper artifacts

The v0.1.1 arXiv-matched release includes the exact ProofDiff outputs and sanitized run metadata used in the paper, including model and version, settings, and dates. Model-backed stages are nondeterministic, so a later rerun may differ even when the same inputs and settings are used. The same software-and-artifact snapshot is archived on Zenodo under the version DOI 10.5281/zenodo.23930759. The concept DOI 10.5281/zenodo.23930758 resolves to the latest archived version.

Citation

Citation metadata for the software and accompanying paper is provided in CITATION.cff. This repository is published at https://github.com/VIDA-NYU/proofdiff-public; the paper release is v0.1.1, published on 2026-11-03. For the exact v0.1.1 software and paper artifacts, cite 10.5281/zenodo.23930759. The arXiv identifier will be added once the paper record exists.

License

• Software source code, tests, configuration, and package metadata are available under the MIT License. See LICENSE.
• Documentation, schemas, original example materials, and other non-code artifacts are available under CC BY 4.0. See LICENSE-CONTENT.
• Third-party material remains under its original terms. See THIRD_PARTY_NOTICES.md.