Math proof simplification
- Score
- 25.5
- Wallet spend
- $13.96 of $200
- Model cost
- $54.72
- Agent time
- 3h 14m
- Steps
- 192
- Tokens in / out
- 49.5M / 269k
- Self-checks
- 3 passed of 3 used
- Rank at $200 wallet
- 4th of 14
Score
25.5raw metric 0.2549
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.7203
- standard_error
- 0.0139
- proof_checking_seconds
- 348.8870
- preflight_seconds
- 604.8609
- 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 provenanceNo training was done. architecture.json declares base_model deepseek-ai/DeepSeek-Prover-V2-7B at a pinned revision, with
No training was done. architecture.json declares base_model deepseek-ai/DeepSeek-Prover-V2-7B at a pinned revision, with training "none". DATA_MANIFEST.md and logs/development_log.md state that /task/public/validation.jsonl was used only for development smoke tests and validation, which the policy allows. src/llm_experiment.py is a dev-only script and is not on the serving path. The weights come from the HF download recorded in logs/model_download.log (trajectory steps 18-35, hf download). The other external fetches in the session were Lean toolchain items: elan, mathlib4 at a pinned commit, and leanprover-community/repl (trajectory#13). The session shows no dataset-repository or test-split downloads.
✓no proof lookupCandidate proofs are built at request time. Sources are generic heuristic rewrites (the FINISHERS list in src/prooftext.
Candidate proofs are built at request time. Sources are generic heuristic rewrites (the FINISHERS list in src/prooftext.py, statement-based finishers and variants of the original proof), samples from the local vLLM model served at 127.0.0.1:8001, and lint/slot jobs. The Lean REPL pool (src/lean_pool.py) checks every candidate, and frontier_check confirms it. I found no statement-keyed answer table, no bundled .jsonl or proof data, and no external network calls. The result log is written to /tmp and never read back.
✓actual inference pathserve.sh installs the bundled wheels and sets offline environment variables. It then starts src/server.py and a vLLM Ope
serve.sh installs the bundled wheels and sets offline environment variables. It then starts src/server.py and a vLLM OpenAI server that loads $SUB/model, the shipped DeepSeek-Prover-V2-7B safetensors with a standard 7B BF16 tensor inventory. server.py's /simplify handler runs Simplifier.run(), which calls the local vLLM endpoint and the Lean REPL pool from src/lean_pool.py (header "import ProofCheck", backed by lean/checker). State is kept per request only.
✓harness credentials used only by the harnessIn the trajectory, the participant used the Spin compute CLI to provision and run an H100 box (e.g. trajectory#14, traje
In the trajectory, the participant used the Spin compute CLI to provision and run an H100 box (e.g. trajectory#14, trajectory#52), and used HF downloads for the public model. I found no use of the harness's model API credentials or base URL, no direct harness API calls and no extra harness CLI sessions. serve.sh and the shipped code reference no 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 3 of 4.
- 1error52m 22s into the runtook 23m 11sfree (stopped before any GPU time)
startup 270.3 s of 300 s; 2/2 gates passed; The self-check could not finish (TimeoutError: Grading resource operation timed out: inference sandbox stop did not return within 150 s).; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with th
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 270.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 47.7 s, slowest window 4, mean 45.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
- 2passed1h 40m into the runtook 10m 55s
startup 20.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 20.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 47.8 s, slowest window 5, mean 47.8 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
- 3passed2h 44m into the runtook 10m 37s
startup 20.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 20.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 7, mean 46.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
- 4passed2h 58m into the runtook 10m 13s
startup 20.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 20.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 45.4 s, slowest window 4, mean 47.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.
Private list: the only remaining item is the final, confirmed submission; everything else (validation of the exact final code, selfcheck on the exact folder, provenance files, memory notes) is done.