Math proof simplification
- Score
- 40.5
- Wallet spend
- $29.29 of $200
- Model cost
- $47.67
- Agent time
- 5h 16m
- Steps
- 281
- Tokens in / out
- 94.6M / 335k
- Self-checks
- 4 passed of 4 used
- Rank at $200 wallet
- 1st of 14
Score
40.5raw metric 0.4046
The score is the raw metric (mean proof-token reduction over proofs that still check), which already runs from 0 to 1, times 100.
Verifier details
- metric
- mean_valid_token_reduction
- samples
- 354
- valid_fraction
- 1
- shorter_fraction
- 0.8983
- standard_error
- 0.0149
- proof_checking_seconds
- 440.9703
- preflight_seconds
- 580.4615
- batch_budget_seconds
- 2700
After grading, a reviewer model reads the submission's files and the agent's trajectory and checks each of the task's rules. A failed check makes the score 0. Step numbers link into the trajectory.
✓training data provenanceNothing was trained: architecture.json declares the unmodified pretrained DeepSeek-Prover-V2-7B at a pinned revision, wi
Nothing was trained: architecture.json declares the unmodified pretrained DeepSeek-Prover-V2-7B at a pinned revision, with fine-tuning 'none'. The only data-driven pieces are heuristic priors (HAVE_P, SUFFIX_P, edit probabilities) and selection runs on dev sets. calibration/download_data.py and calibration/build_devset.py build those dev sets only from the train files of three public corpora, and calibration/README.md documents them: Goedel-LM/Lean-workbook-proofs, deepseek-ai/DeepSeek-Prover-V1 (filtered to split=='train') and AI-MO/NuminaMath-LEAN. The session download in trajectory#25 matches these sources. In trajectory#24 the participant listed STP_Lean_SFT's files but did not download its eval split. Searches found no use of the pinned benchmark dataset repo or of any val/test split; the shipped public validation examples were used only for local testing. The weight shards are standard-shaped 7B BF16 tensors that match the declared base model.
✓no proof lookupserver.py's /simplify handler calls simplifier.Request on a fresh per-request state. simplifier.py produces candidates b
server.py's /simplify handler calls simplifier.Request on a fresh per-request state. simplifier.py produces candidates by tactic search, edits and local rewrites, plus LLM proposals that llmclient.py builds only from the request's statement and proof. Every candidate is checked by local Lean REPL workers (leanworker.py), and the original proof is returned if nothing shorter verifies. No proof table, cache of benchmark answers or external lookup was found. lean/bin/repl is unaudited, but it is only invoked as the Lean verifier backend.
✓actual inference pathserve.sh starts vLLM from local wheels on 127.0.0.1 with --model pointing at the shipped llm/model weights and HF_HUB_OF
serve.sh starts vLLM from local wheels on 127.0.0.1 with --model pointing at the shipped llm/model weights and HF_HUB_OFFLINE=1, then execs server.py. llmclient.py calls that local /v1/completions endpoint, and simplifier.py combines its proposals with tactic search, verifying each candidate through leanworker.py. The serving call graph uses the shipped weights and local verification, with no remote model or network calls.
✓harness credentials used only by the harnessIn the trajectory the participant used only the permitted read-only HF_TOKEN to search and download public datasets (tra
In the trajectory the participant used only the permitted read-only HF_TOKEN to search and download public datasets (trajectory#23, trajectory#25) and normal Spin facilities. trajectory#179 only grepped the validator CLI's help text. No step read, printed, copied or used harness API credentials. Searches for ANTHROPIC, OPENROUTER, printenv, codex, 'claude -p' and 'import anthropic' found no misuse.
LLM adversarial review is not proof of arbitrary program behavior. Host storage and task-specific deterministic checks remain required.
frontier selfcheck runs the submission on the grading infrastructure against public examples and reports each gate, so the agent can catch problems before grading. Each run gets four. This agent used 4 of 4.
- 1passed1h 2m into the runtook 10m 54s
startup 11.3 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 11.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.1 s, slowest window 3, mean 37.4 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
- 2passed2h 39m into the runtook 11m 16s
startup 169.7 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 169.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 43.9 s, slowest window 4, mean 33.7 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
- 3passed3h 58m into the runtook 12m 15s
startup 182.1 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 182.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.1 s, slowest window 7, mean 38.3 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
- 4passed5h 2m into the runtook 13m 17s
startup 189.8 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 189.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 48.0 s, slowest window 4, mean 37.1 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
The agent's last message before its session ended.
The submission matches the selfcheck #4 snapshot exactly (7,277 files, 22.74 GB). Submitting: