Math proof simplification
- Score
- 29.8
- Wallet spend
- $9.11 of $50
- Model cost
- $38.17
- Agent time
- 2h 47m
- Steps
- 279
- Tokens in / out
- 77.7M / 269k
- Self-checks
- 3 passed of 3 used
- Rank at $50 wallet
- 2nd of 14
Score
29.8raw metric 0.2977
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.7881
- standard_error
- 0.0137
- proof_checking_seconds
- 420.3292
- preflight_seconds
- 660.7022
- 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, fine-tuned, calibrated or selected on any data. architecture.json sets training_data to "none (no t
Nothing was trained, fine-tuned, calibrated or selected on any data. architecture.json sets training_data to "none (no training, fine-tuning, calibration or selection corpus was used; the base model is used as released)" and lists no training_evidence_files. The model is the public deepseek-ai/DeepSeek-Prover-V2-7B at pinned revision a8d9e144…. It was fetched with huggingface snapshot_download, which is recorded in logs/model_download.log and the trajectory. The HF cache tree metadata matches that revision. During development the participant used the public validation set shipped with the task, but only to test the server. I found no training run anywhere in the trajectory.
✓no proof lookupEvery output proof is built when the request arrives. server.py passes the request's statement and proof to Search(...).
Every output proof is built when the request arrives. server.py passes the request's statement and proof to Search(...).run(). search.py then runs deterministic deletion, closer and truncation passes, and every candidate is checked by the Lean 4 worker pool in lean_pool.py. llm.py adds proposals from the local model on 127.0.0.1, prompted with the request statement, and these are kept only if Lean verifies them. Caches are created per Search instance, so they last only for one request. No server module loads a dataset or proof table: the only file opens are log files and the pip install log. I found no evidence of a bundled answer store or of fetching proofs from outside sources.
✓actual inference pathThe serving call path is: serve.sh runs server/server.py; POST /simplify calls simplify(), which calls Search.run(). Sea
The serving call path is: serve.sh runs server/server.py; POST /simplify calls simplify(), which calls Search.run(). Search.run() uses LeanPool (persistent CheckServer.lean workers on the shipped Lean toolchain and Mathlib) and LLMProposer. LLMProposer starts vLLM on the shipped local weights in model/DeepSeek-Prover-V2-7B with HF_HUB_OFFLINE=1 and queries 127.0.0.1. Wheels are installed offline with --no-index. A final frontier_check confirms the result before it is returned. If the search crashes, the server returns the original proof, which is a valid output. The weight files listed in the weight inventory are the ones that vLLM loads.
✓harness credentials used only by the harnessThe participant's session used only what was allowed. HF_TOKEN was used for the model download via snapshot_download, an
The participant's session used only what was allowed. HF_TOKEN was used for the model download via snapshot_download, and the Spin CLI was used to lease a GPU and to view openrouter help. When the participant listed the environment, every value was masked with sed. My searches found no use of ANTHROPIC or other API keys, no direct API client imports, no printenv dump of secrets, and no use of credentials in the shipped code. The server makes no external network calls.
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.
- 1passed34m 6s into the runtook 6m 9s
startup 13.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 13.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 43.5 s, slowest window 4, mean 36.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
- 2passed1h 29m into the runtook 10m 36s
startup 19.4 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 19.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 43.7 s, slowest window 4, mean 36.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
- 3passed2h 37m into the runtook 9m 21s
startup 18.9 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 18.9 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 44.9 s, slowest window 7, mean 38.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
The agent's last message before its session ended.
All 12 symlinks are relative, resolve inside the folder, and are not dangling, matching what the three passing selfchecks already validated. Handing in now.