OpenMathProof

Description

Natural-language proof search using precise theorem statements from the pinned OpenAI mathematics collection. The agent receives the mathematical assertion, including the assumptions and definitions needed to understand it. The corresponding OpenAI solution supplies the evidence for a private, task-specific marking scheme.

Each scheme contains major mathematical checkpoints and finer subclaims for partial credit inside those checkpoints. Both levels stay private. There is one final proof submission and no intermediate-reward tool.

Preparation targets all 722 source manuscripts and classifies their 8,421 theorem/proposition/corollary occurrences. Distinct principal results become tasks; restatements, auxiliary results and cited external results are explicitly accounted for. The final task count comes from completed preparation, not from the number of manuscripts or every auxiliary lemma. data/manifest.json records the current state and, after publication, the final counts. A full publication refuses to proceed while any manuscript remains unprepared.

Private preview, 2026-10-08: the packaged corpus contains 509 tasks from 197 manuscripts, with 2,622 major checkpoints and 12,278 fine subclaims. Another 525 manuscripts remain unprepared. This release uses the explicit partial-packaging option and is marked development_partial; it does not represent full corpus coverage. Preparation stopped at its authorized budget limit. No batch is running, and unmetered local model calls remain disabled by PAID_RUNS_DISABLED.

Capabilities

• Research-level proof generation with standalone statements.
• Precise handling of quantified scope, hypotheses, exceptional cases and effectiveness.
• Partial credit for specific mathematical sub-results, even when a major argument is unfinished.
• Full credit for valid independent proof methods.

Compute Requirements

The environment has no agent sandbox. It loads compressed manuscript text and prepared marking schemes. Large grading references are reviewed in overlapping parts before final assessment; memory, episode duration and average cost have not been benchmarked.

Offline preparation uses gpt-5.6-sol for statement/rubric generation and gpt-5-mini for independent source-alignment audits. Runtime grading uses gpt-6-sol with reasoning_effort="medium" for both reference-part reviews and final verdicts. No temperature parameter is supplied. Preparation reuses cached responses, writes small compressed records and preserves a 20 GiB disk reserve. It needs no Docker build or Lean installation.

License

Apache-2.0, matching the upstream collection.

Tasks

The preparation process separates independent principal statements into tasks. It retains the required local definitions and conditional assumptions in the opening prompt, without supplying the proof route. It does not use the abstract as the task statement and has no optional statement-context tool.

The preview has 373 training, 46 validation and 90 test tasks. Splits are train, validation, and test, using the deterministic result-family assignment shared with OpenMathLean. All tasks in one of the 372 source families stay in the same split. Public task specifications contain only an opaque ID; server-side lookup supplies the authoritative statement and rubric.

Run python build/status.py to inspect current preparation coverage. The example artifacts in examples/ are generated records, not invented illustrations. The Catalan example exposes its private rubric for developer inspection; it is never supplied to a solving agent.

Reward Structure

The private major checkpoints have positive integer weights totaling seven. Each has precise mathematical content, evidence requirements and source quotations. Fine subcheckpoints identify smaller results supporting a particular major checkpoint, with relative weights within that parent.

For each major checkpoint of weight w:

if its complete mathematical obligation is proved:
    credit = w
else:
    credit = 0.5 * w * (proved subcheckpoint weight / total subcheckpoint weight)

reward = sum(credit) / 7

The half-budget for subclaims is an explicit, uncalibrated design choice: it rewards useful partial work while reserving credit for establishing the major conclusion. A fully completed checkpoint replaces its subcredits, so the same work cannot be counted twice. Dependencies prevent credit for downstream assertions resting on unproved premises. Independently established subclaims retain their credit. Concrete mathematical failure rules invalidate only specified major obligations and their dependants.

The judge must identify evidence from the submitted proof for every claim marked proved. The candidate is divided into labeled literal passages; the judge selects passage IDs, and Python retrieves the original candidate text. It cannot select evidence from the private reference. Python validates the checkpoint IDs, evidence and dependency structure, then computes the score; the judge does not invent a scalar reward. A complete valid independent proof receives seven points even when it does not establish reference-specific intermediate lemmas. Partial independent arguments must map to equivalent prepared obligations; otherwise the judge withholds an uncertain assessment instead of inventing credit.

If the judge marks a major claim proved while also denying its reference prerequisites or applying a failure that invalidates it, a neutral review checks whether this reflects a real gap or a valid alternative route. The review can increase or decrease credit. Each submission call allows at most three final-judge attempts in total, shared across malformed output, truncation, uncertainty, provider failures and consistency reviews. Unresolved assessments remain pending; they never become a fallback zero.

In the live polynomial example, the first major checkpoint is worth one point and requires two algebraic identities. Its two fine subclaims have equal weight. Proving only x² + y³ = hs therefore earns 0.5 × 1 × 1/2 = 0.25 points, or a normalized reward of approximately 0.0357. Proving the complete major obligation would earn one point. The recorded live checks gave 0/7 to an unsupported assertion, 0.25/7 to the single-identity proof, and 7/7 to the source manuscript. These are observed model judgments on three submissions, not a calibration study.

This is LLM assessment, not formal verification. Source-alignment audits do not establish that the source proof is correct. The grader treats the manuscript as fallible evidence and checks the candidate independently. Successful grading ends the episode; subsequent submissions earn zero additional reward. The policy receives only the final score and assessment status. Free-form judge feedback stays private because it can accidentally reveal the reference's proof route.

Grading failures return a normal tool result with reward=null, finished=false and metadata.status="grading_pending", preserving the session instead of raising a tool error. The original submitted proof is fixed on the first call. Call submit_proof(proof="retry grading") to resume; any later input grades the saved original, so there is no need to regenerate it. Successful source-part reviews are retained, and only missing reviews are requested again. The proof, reviews and latest private correction are held in memory for that session, not durably across a container restart or session deletion. A training harness must treat pending as unfinished and resume the same session, not coerce null to a scored zero or discard it as a terminal outcome.

Each missing reference part gets at most two attempts per tool call (three parts can run concurrently). Reference output starts at 32,000 tokens and rises to 64,000 after truncation; final-verdict output starts at 24,000 and rises by 12,000 after truncation, up to 48,000. The higher limit is retained on resumption. Transient provider failures use bounded backoff; bad credentials, invalid requests and exhausted credit return pending immediately without repeated automatic calls. Each request times out after ten minutes. SDK retries are disabled, and all requests use standard pricing. These bounds apply per tool call, not to total session spending: a later retry call can make further requests. Genuine validated incorrect proofs can still receive zero; judge failures cannot.

Data

Pinned revision: adc7f1241b42e322a6451854ab7e4b4c146bf78a.

• data/catalogue.json: all 722 manuscripts, source hashes and family assignments.
• data/references.json.gz: complete expanded manuscript LaTeX, private to the server.
• data/source_repairs.json: provenance for ten sources initially represented by preambles or a PDF wrapper, repaired from pinned text files.
• data/cards/: prepared statements, major/fine rubrics, source quotations, inventory decisions and source-audit records per manuscript.
• data/prepared.json.gz: atomically published runtime tasks and private rubrics.
• data/manifest.json: published coverage and split counts.

Runtime data is bundled; there are no startup downloads. OPENMATHPROOF_DATA_DIR can select a different server-side copy. Do not expose these private files to the agent.

To prepare from the existing bundled references:

# Requires an existing ledger created for an explicitly authorized budget.
python build/curate.py --secrets-file /path/to/private/.env \
  --budget-ledger /path/to/private/authorized-ledger.json \
  --prioritize-cached --concurrency 1
python build/package_tasks.py
python build/status.py

build/spending.py reserves the worst-case standard-tier cost before each network attempt, under a file lock. It uses the model's entire context allowance and requested maximum output, the higher cache-write/long-context prices, and an additional 25% allowance. Confirmed usage releases only the unused part of the reservation; accounting still assumes all input incurs cache-write prices. Errors, cancellation, missing usage and crashes retain the full reservation. This conservative ceiling is not a provider invoice and can stop a run below its nominal budget.

The ledger survives process restarts and is stored outside the response cache. Its creation refuses to overwrite an existing ledger. SDK retries are disabled; every explicit retry must reserve funds again. Unknown models, premium service tiers, unpriced options and expired pricing policies fail before dispatch. In-flight requests finish before a budget cutoff when possible. A local spending authorization is shared across runs and must never be renewed merely by restarting a command. Preserve build/budgets/ during cleanup.

A preparation batch writes build/budgeted-run.log and produces build/budgeted-run.json when it stops. A local build/finalize_run.py watcher updates coverage/status records and writes build/budgeted-outcome.json after that report arrives. It makes no model calls and only publishes the runtime corpus if all 722 manuscripts pass normal packaging checks.

The GPT-6 Sol pricing entry was verified against its official model page on 2026-10-11. Existing version-1 ledgers are upgraded only by adding these prices; their authorization, charges and outstanding reservations are preserved. Earlier pricing was checked against the official Sol and mini pages on 2026-10-08; this pricing policy expires on 2026-11-20 and requires review thereafter. Offline tests cover concurrent reservations, persistence, cutoff before dispatch, retained failed-request reservations and usage validation. Exhausted provider credit is independently fatal. Temporary rate limits use bounded backoff; output truncation can trigger a larger reserved output limit. Concurrency defaults to one and is capped at four. Runtime servers and the old agent scripts do not use this local preparation ledger; their unmetered entry points remain on hold for local paid testing.

The private file supplies OPENAI_API_KEY or CHAT_API_KEY; it is read at runtime and never copied into dataset files. The explicit --allow-partial packaging option produces this private preview and marks incomplete coverage. Normal packaging requires every manuscript. To reconstruct the source corpus from a pinned checkout, first run python build/prepare_corpus.py --source /path/to/checkout.

Tools

submit_proof(proof=...): submit the complete natural-language argument, including honestly stated partial progress. Input is limited to 500,000 characters to accommodate long research arguments. This is the only policy tool. If grading remains pending, repeat this tool with proof="retry grading"; the original argument is retained. Token-heavy inputs can still exceed the grader's context limit; a permanent context rejection requires operator intervention, not repeated identical requests.

Time Horizon

One successfully graded proof. Grading retries always assess that same proof and provide no mathematical feedback or intermediate reward. There are no intermediate proof revisions, process rewards, shell tools or exposed private-checkpoint feedback before the final submission. No average solving time or success rate has been measured.

Environment Difficulty

The sources contain research claims at different stages of verification. Neither inclusion in this corpus nor a high LLM score establishes their truth. Automatic preparation can still miss scope or notation issues; expert review and grader calibration remain necessary before strong benchmark claims.

Other Environment Requirements

Pass the grader credential through session secrets as openai_api_key (or set OPENAI_API_KEY). The judge follows OPENAI_BASE_URL, so an OpenAI-compatible gateway that serves gpt-6-sol can host it. A chat_api_key secret, CHAT_API_KEY or CHAT_BASE_URL gives the judge a dedicated endpoint instead (default https://api.openai.com/v1); the build/ scripts use that channel.

Local Development

pip install -r requirements.txt
python -m pytest golden_tests.py build/test_grading_recovery.py build/test_spending.py -q
python server.py
python test_agent.py --split test --index 0

The server listens on port 8080. test_agent.py uses the Responses API and defaults to gpt-5.6-sol against the local server. See VALIDATION.md for completed checks and their limits.

The budgeted local alternative is build/run_examples.py --budget-ledger PATH --secrets-file PATH --example noncoordinate --example catalan. It creates an isolated development package, obtains the actual environment prompt, runs one Sol Responses-API submission per example and sends it through the real environment's GPT-6 Sol grader. Both policy and grading calls share the ledger. It saves each policy response before grading and reuses it on restart. Results appear in examples/*-solver.json; the reference and private rubric are never included in the solving request.

Safety

The grader treats candidate and source text as untrusted data and keeps reference material private. Evidence-quotation checks constrain attribution but cannot establish mathematical validity or eliminate prompt-injection risk.

Citations

@misc{openai_math_2026,
  author = {{OpenAI}},
  title = {Mathematics Manuscript Collection},
  year = {2026},
  url = {https://github.com/openai/math},
  note = {Revision adc7f1241b42e322a6451854ab7e4b4c146bf78a}
}
@dataset{fineproofs_rl,
  author = {{LM Provers}},
  title = {FineProofs-RL},
  url = {https://huggingface.co/datasets/lm-provers/FineProofs-RL}
}

FineProofs-RL informs the problem-specific checkpoint approach; the manuscript-derived rubrics and hierarchical partial-credit rule here are a new adaptation. Framework guidance: OpenReward rubrics and chat backends.