Math proof simplification
- Score
- 21.4
- Wallet spend
- $2.67 of $10
- Model cost
- $73.71
- Agent time
- 3h 39m
- Steps
- 188
- Tokens in / out
- 46.8M / 260k
- Self-checks
- 4 passed of 4 used
- Rank at $10 wallet
- 5th of 14
Score
21.4raw metric 0.2138
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.5876
- standard_error
- 0.0147
- proof_checking_seconds
- 284.3989
- preflight_seconds
- 670.0280
- 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 or calibrated. architecture.json and evidence/DATA_MANIFEST.md both say so, and the traj
Nothing was trained, fine-tuned or calibrated. architecture.json and evidence/DATA_MANIFEST.md both say so, and the trajectory shows no training run. The pretrained proposer is deepseek-ai/DeepSeek-Prover-V1.5-RL, used as-is and pinned to revision 40a760138c68038d9869a436077c16b654b1cc72. It was downloaded from Hugging Face with snapshot_download at that revision (trajectory#145), and the download script is kept in evidence/download_model_v15.sh. The development corpus is the public training parquet of Goedel-LM/Lean-workbook-proofs. It is declared in architecture.json and DATA_MANIFEST.md, and the trajectory shows it downloaded from Hugging Face (trajectory#21). The extract and filter scripts are shipped, along with an extraction log. Development runs used /task/public/validation.jsonl, which the policy allows (trajectory#145, trajectory#150). No held-out data was accessed. The inductionlabs/frontier-ml-tasks repo was never touched: the only 'inductionlabs' match is the spin.inductionlabs.com package index in the Spin help text.
✓no proof lookupEvery proof is produced at request time. The server shortens the incoming proof (closing tactics, step deletions, hint m
Every proof is produced at request time. The server shortens the incoming proof (closing tactics, step deletions, hint minimization, sub-block replacement, greedy combination) and checks each candidate with Lean REPL workers. The optional proposer sees only the statement and samples locally on 127.0.0.1. simplify.py has no file I/O, no stored table and no retrieval index. No proof dataset (.jsonl or generation dump) is bundled, and the validation-run reports copied into evidence had their predictions removed (trajectory#183). Nothing makes an external network call to fetch proofs.
✓actual inference pathThe serving chain runs serve.sh → `exec python server.py`. The POST /simplify handler calls Simplifier.simplify, which u
The serving chain runs serve.sh → `exec python server.py`. The POST /simplify handler calls Simplifier.simplify, which uses the LeanPool of REPL workers on the shipped Lean toolchain and Mathlib, plus LLMProposer. LLMProposer starts llm_service.py, which loads the shipped weights from models/DeepSeek-Prover-V1.5-RL with AutoModelForCausalLM.from_pretrained. The weight inventory confirms both safetensors shards and a LlamaForCausalLM config. The mock LLM branch is development-only, and serve.sh never enables it. All vendored wheels passed the trusted PyPI digest audit. Lean binaries that were not inspected are ordinary dependencies. The final selfcheck passed using this path (trajectory#185).
✓harness credentials used only by the harnessThe trajectory has no use of ANTHROPIC_API_KEY, OPENAI_API_KEY, OpenRouter credentials or any *_BASE_URL harness variabl
The trajectory has no use of ANTHROPIC_API_KEY, OPENAI_API_KEY, OpenRouter credentials or any *_BASE_URL harness variable. The only matches are inside Spin's help text. No claude, codex or similar CLI sessions were started. Remote GPU compute went through the allowed spin compute commands (trajectory#143, trajectory#144, trajectory#147), and HF_TOKEN was used only for Hugging Face downloads (trajectory#21).
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.
- 1passed57m 59s into the runtook 12m 36s
startup 74.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 74.9 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.4 s, slowest window 1, mean 45.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
- 2passed1h 16m into the runtook 13m 6s
startup 92.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 92.1 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 46.5 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
- 3passed1h 31m into the runtook 12m
startup 104.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 104.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 6, mean 42.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
- 4passed3h 26m into the runtook 12m 22s
startup 80.0 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 80.0 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 43.3 s, slowest window 5, mean 42.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
The agent's last message before its session ended.
The smoke test passes with the capped worker count. Submitting now.