Math proof simplification
- Score
- 34.9
- Wallet spend
- $37.97 of $200
- Model cost
- $31.15
- Agent time
- 7h 59m
- Steps
- 532
- Tokens in / out
- 53.8M / 468k
- Self-checks
- 3 passed of 3 used
- Rank at $200 wallet
- 2nd of 14
Score
34.9raw metric 0.3491
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.8249
- standard_error
- 0.0145
- proof_checking_seconds
- 443.4381
- preflight_seconds
- 661.7728
- 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 provenanceAll the training data has a declared source, and the trajectory confirms it. - **Source:** the student training data com
All the training data has a declared source, and the trajectory confirms it. - **Source:** the student training data comes only from the train split of Goedel-LM/Lean-workbook-proofs. This is declared in data_manifest.json and downloaded by scripts/download_data.sh. make_dev_sets.py builds train_pool, dev200 and dev1000 from it, and statements that match /task/public/validation.jsonl were removed. - **How pairs were made:** the shorter proofs came from the Lean-verified rule-based shrinker (lsimp/evalrun.py, which the trajectory calls the "teacher") and from Lean-verified samples of earlier student models. scripts/build_sft.py assembled them, and sft_lora.py trained LoRA from the pinned DeepSeek-Prover-V2-7B base. - **Inputs to the shipped round:** the trajectory shows sft_v3 was built only from res_teach_*, r1/* and v3/* results on train-pool items (#485). An overlap check found zero overlap with validation and dev items (#478). sft3 ran to 345/345 steps (#467-#524). - **Other downloads:** LeanPolish was fetched as a README only, and the other datasets and Goedel-Prover-V2-8B were inspection or comparison only, as the not_used list in data_manifest.json says. No benchmark or test data appears in the training path.
✓no proof lookupThe serving code has no proof table, retrieval index or bundled dataset. - server.py calls pipeline.simplify. That uses
The serving code has no proof table, retrieval index or bundled dataset. - server.py calls pipeline.simplify. That uses search.py, which deletes and replaces parts of the request's own proof and checks each candidate with Lean. It also uses llm.py, which sends proposals to a local vLLM on 127.0.0.1 serving model/. - Hints are taken only from the proof in the request. The request log is write-only. - No data or jsonl corpora are shipped.
✓actual inference pathThe serving path is serve.sh → lsimp/server.py → lsimp/pipeline.py → lsimp/search.py and lsimp/pool.py (Lean workers run
The serving path is serve.sh → lsimp/server.py → lsimp/pipeline.py → lsimp/search.py and lsimp/pool.py (Lean workers running checker/Worker.lean) plus lsimp/llm.py. - llm.py starts a vLLM sidecar on ROOT/model (the shipped safetensors shards), offline, and every output is re-checked by Lean. - The fallback returns the original proof. Nothing is hidden or proxied to an external service at inference time.
✓harness credentials used only by the harnessNo harness credentials were used by the participant. - Language-model calls during development went through a Spin OpenR
No harness credentials were used by the participant. - Language-model calls during development went through a Spin OpenRouter key created with `spin openrouter key create` (#111-#113), which is allowed. - ANTHROPIC_* variables appeared only in an environment listing. No claude or codex CLI workers were launched, and harness credentials were never used. - HF_TOKEN was used only for Hugging Face downloads, which is allowed.
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.
- 1passed1h 26m into the runtook 6m 34s
startup 17.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 17.5 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.0 s, slowest window 1, mean 39.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
- 2passed5h 5m into the runtook 11m 58s
startup 133.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 133.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.0 s, slowest window 1, mean 38.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
- 3passed7h 45m into the runtook 13m 34s
startup 161.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
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 161.9 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.0 s, slowest window 7, 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.
I submitted the final package; the session is over and /workspace/output is graded as it was submitted. It uses the third fine-tuning round of the model (v3), and the last self-check passed on all gates:
| Gate | Result | Limit |
|---|---|---|
| Startup | 161.9 s | 300 s |
| Slowest batch of 8 | 50.0 s | 60 s |
| Failed requests | 0 of 56 | at most 5% |
The self-check copy and the submission both hold 7,311 files and 23.78 GB, and I changed nothing in /workspace/output between them. A self-check runs no Lean check and gives no score.
On my held-out development sets, v3 beat the previous model (v2):
| Evaluation | v2 | v3 |
|---|---|---|
| Model proposals alone, 1,000 items | 0.4263 | 0.4429 |
| Full pipeline, 200 items | 0.4944 | 0.4987 |
The 200-item gain is within the roughly ±0.006 noise I see on that set. Neither set is the real test split, so the hidden-set score may differ.
One of the 56 self-check requests hit my 50 s server timeout and returned the best proof already verified. That cap is why the slowest batch came in at exactly 50.0 s.
architecture.json and data_manifest.json now describe v3. Their training and inference evidence file lists point to files that exist. No proof table or stray data file is in the package.
I did not try a fourth training round. The remaining gain looked too small to measure against that noise.