API documentation

Quickstart

1. Choose a monthly data plan and complete checkout.
2. Create and copy a key under Your API keys. Copy new keys before leaving this page. Full keys are shown only when created.
3. Replace the placeholder below with your key and make a request.

export MATHDB_API_KEY='YOUR_MATHDB_KEY'

curl 'https://mathdb.com/api/data/problems?limit=2' \
  -H "Authorization: Bearer $MATHDB_API_KEY"

List responses contain an items array and a next_cursor. A null cursor means you have reached the end.

Authentication

Send Authorization: Bearer YOUR_MATHDB_KEY with every data API request. Keys start with mdb_ and grant read-only data access while your subscription is active.

Keep keys in server-side environment variables, never in browser code or public repositories. Revoke a key from your account if it is exposed. Each Business teammate uses their own login and keys.

Endpoint reference

All paths below are relative to https://mathdb.com. Responses use JSON.

Verify a Lean proof

Submit a problem description and a Lean proof file containing the theorem it proves. MathDB uses Jiaxin’s MathDB-Lean evaluator: MathDB extracts the selected theorem using the evaluator’s scanner, Claude checks that it matches the description, and Lean verifies the proof. Both checks must pass. Use your existing Individual or Business subscription API key.

import os
import time
from pathlib import Path
import requests

base = "https://mathdb.com"
headers = {"Authorization": f"Bearer {os.environ['MATHDB_API_KEY']}"}
response = requests.post(f"{base}/api/lean/v1/proofs", headers=headers, json={
    "submission": Path("proof.lean").read_text(encoding="utf-8"),
    "prose": Path("problem.txt").read_text(encoding="utf-8"),
}, timeout=30)
response.raise_for_status()
job = response.json()
deadline = time.monotonic() + 2100
while job["status"] in ("queued", "running"):
    if time.monotonic() > deadline:
        raise TimeoutError("Save the job ID and check it again later.")
    time.sleep(5)
    response = requests.get(base + job["poll_url"], headers=headers, timeout=30)
    response.raise_for_status()
    job = response.json()
print(job["result"] if job["status"] == "completed" else job["error"])

curl 'https://mathdb.com/api/lean/v1/formats' \
  -H "Authorization: Bearer $MATHDB_API_KEY"

Send file contents as JSON strings, rather than GitHub URLs or folders. No separate statement file or MathDB problem ID is needed. If your proof file contains multiple theorems, add theorem with the fully qualified name to check. The LLM assessment can be wrong, and an inconclusive result is not a pass. Results include separate faithfulness and proof records. A completed job means a result is available, not that the proof was accepted or a prize was awarded. MathDB’s website verifies submissions against its saved statements internally, without an LLM; that workflow is not a public API endpoint.

Each source is limited to 200,000 UTF-8 bytes. You can submit five checks per ten minutes and keep two in flight per account; additional keys do not increase these limits. Format checks allow 30 requests per minute, and polling allows 60. Checks have a maximum Lean timeout of 900 seconds, with additional time for worker startup. HTTP 503 means the worker or judge is unavailable. Revoking a key, ending subscription access, or removing Business team membership immediately stops access through that key.

Read the next page

Pass the returned next_cursor as after on your next request. Keep your filters unchanged, and stop when the cursor is null. Each page contains at most 100 records.

import os
import requests

headers = {"Authorization": f"Bearer {os.environ['MATHDB_API_KEY']}"}
after = 0
while True:
    response = requests.get(
        "https://mathdb.com/api/data/problems",
        headers=headers,
        params={"after": after, "limit": 100},
        timeout=30,
    )
    response.raise_for_status()
    page = response.json()
    for problem in page["items"]:
        print(problem["number"], problem["title"])
    after = page["next_cursor"]
    if after is None:
        break

Dataset downloads

For bulk analysis, choose a snapshot from GET /api/datasets, then request its download link. Links expire after five minutes; request another if needed. Verify the file against the returned SHA-256 checksum.

curl -X POST 'https://mathdb.com/api/data/snapshots/SNAPSHOT_ID/download' \
  -H "Authorization: Bearer $MATHDB_API_KEY"

Each ZIP includes problems.jsonl, solutions.jsonl, tags.jsonl, manifest.json, and TERMS.txt. Read the snapshot terms and retain source attribution. Private account data, messages, embeddings, and attachments are excluded.

Limits & errors

Both paid plans have no daily or monthly data quota. A shared speed limit of 600 API requests per minute per user protects availability. Multiple keys do not increase that limit.

Non-success responses include a detail field. Handle errors before processing a response as data.