Math proof simplification
- Score
- 0.1
- Wallet spend
- $10.47 of $50
- Model cost
- $0.49
- Agent time
- 1h 4m
- Steps
- 259
- Tokens in / out
- 39.4M / 133k
- Self-checks
- 3 passed of 4 used
- Rank at $50 wallet
- 14th of 14
Score
0.1raw metric 0.0006802
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.0056
- standard_error
- 0.0005
- proof_checking_seconds
- 6.9417
- preflight_seconds
- 588.0792
- 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 provenanceThe submission does no training, fine-tuning, calibration or benchmark-based selection. data_manifest.json and architect
The submission does no training, fine-tuning, calibration or benchmark-based selection. data_manifest.json and architecture.json declare the only learned component: the public pretrained checkpoint deepseek-ai/DeepSeek-Prover-V2-7B, pinned to revision a8d9e14432b2e8dd9df2a4d4e70f1ba9bc8d9b7b. download_model.sh retains the snapshot_download command at that revision, model_download.log is shipped, and the model/ directory holds the standard upstream files (README, LICENSE, HF cache metadata). The manifest states that validation and test splits were not used. In the trajectory, the only use of public inputs was frontier selfcheck for operational gating (trajectory#234-236). No dataset download or training run appears in the trajectory.
✓no proof lookupserver.py builds each answer at request time. It tries a few generic short tactics, then one greedy generation from the
server.py builds each answer at request time. It tries a few generic short tactics, then one greedy generation from the local model (from a prompt built on the statement), then a generic tactic fallback. Every candidate is checked by Lean and accepted only if it is shorter than the original proof. There is no proof table, retrieval index, hash lookup, network access or persistent store keyed on requests. architecture.json says the same, and simplification_metric.py is only the length and policy lexer.
✓actual inference pathserve.sh does an offline pip install from the audited wheels/, unpacks lean-runtime.tar.zst (via unpack_runtime.py) into
serve.sh does an offline pip install from the audited wheels/, unpacks lean-runtime.tar.zst (via unpack_runtime.py) into the Lean bundle, sets HF_HUB_OFFLINE and TRANSFORMERS_OFFLINE, and execs server.py. server.py loads the tokenizer and LlamaForCausalLM from ROOT/model with local_files_only in bf16 on cuda:0, using the shipped safetensors shards (their weight inventories match the 7B architecture). Its /simplify handler calls model.generate and Lean verification. The lean-runtime archive is used only as the Lean/Mathlib toolchain, built from public sources by package_lean.sh and prepare_runtime.sh. Its being uninspected is not by itself a violation.
✓harness credentials used only by the harnessOPENAI_API_KEY appears only in an environment listing whose values are redacted (trajectory#6). No participant command r
OPENAI_API_KEY appears only in an environment listing whose values are redacted (trajectory#6). No participant command reads, exports or sends that key, calls api.openai.com or another model API with it, or runs a codex or harness CLI. Compute use was through the permitted spin CLI (trajectory#9, trajectory#16, trajectory#22), and public HF metadata was fetched without harness credentials.
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.
- 1failed21m 30s into the runtook 12m 27s
startup 124.1 s of 300 s; 0/1 gates passed; failed slowest batch of 8: window 1 of 7: Batch exceeded 60s deadline; score is zero. It was the first traffic after /health, as grading's first window is.; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --
3 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 124.1 s
- ✗slowest batch of 8 · window 1 of 7: Batch exceeded 60s deadline; score is zero. It was the first traffic after /health, as grading's first window is.
- 2passed35m 38s into the runtook 10m 5s
startup 117.5 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 117.5 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 34.9 s, slowest window 1, mean 32.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
- 3passed46m 43s into the runtook 8m 44s
startup 114.6 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 114.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 35.1 s, slowest window 1, mean 33.0 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
- 4passed56m 24s into the runtook 9m 22s
startup 125.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 125.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 36.1 s, slowest window 6, mean 32.9 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.
Submitted /workspace/output at 2026-10-02 13:42:50 UTC.
The final frontier selfcheck passed: startup was 125.7 seconds, the slowest batch of eight took 37.3 seconds, and 0 of 56 requests failed. Selfcheck checks response handling and speed; it does not score proof correctness or simplification.