Math proof simplification
- Score
- 20.1
- Wallet spend
- $7.47 of $10
- Model cost
- $6.89
- Agent time
- 4h 11m
- Steps
- 323
- Tokens in / out
- 113.5M / 431k
- Self-checks
- 4 passed of 4 used
- Rank at $10 wallet
- 6th of 14
Score
20.1raw metric 0.2012
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.5960
- standard_error
- 0.0131
- proof_checking_seconds
- 255.9671
- preflight_seconds
- 587.3371
- 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 in the submission is trained. architecture.json says it does no fine-tuning, training or calibration, and the mo
Nothing in the submission is trained. architecture.json says it does no fine-tuning, training or calibration, and the model is Goedel-Prover-V2-8B used as-is. The pinned revision was downloaded with snapshot_download (trajectory#37), and provenance/logs/model_download.log records that download. The one data-driven choice (prompt style, sample counts, search budgets) was made on 128 items from the AI-MO/NuminaMath-LEAN train split. That corpus is declared in provenance/data_manifest.json with its revision and sha256, and its download is retained in provenance/download_numina_train.sh and trajectory#29. That is a public train split, which the policy allows. I found no download of inductionlabs/frontier-ml-tasks or lean-simplification, and no use of any validation or test split of a public benchmark. The only other data touched was /task/public/validation.jsonl, the shipped public examples, and it was used only to check that the checker accepts the original proofs.
✓no proof lookupProofs are made at request time. The do_POST handler in server/server.py queues a Job built from the request's statement
Proofs are made at request time. The do_POST handler in server/server.py queues a Job built from the request's statement and proof. Engine.generate then samples candidates from the vLLM model using three prompts: shorten, prove and brief. solve() tries the fixed generic closer tactics in proof_tools.CLOSERS, fast-checks candidates in the Lean REPL, shrinks the best one greedily, and confirms it with frontier_check. If nothing passes, the input proof is returned. No table, cache, index or embedding store maps statements to proofs. The dev JSONL files under provenance/dev_selection hold NuminaMath train items, and the server never imports them. serve.sh sets HF_HUB_OFFLINE/TRANSFORMERS_OFFLINE, and I found no network calls in the server code. FrontierFlags.lean is 584 bytes and only rejects unsafe or partial declarations (trajectory#243).
✓actual inference pathserve.sh installs the vendored wheels and runs server/server.py with MODEL_DIR set to the shipped model/ folder. Engine
serve.sh installs the vendored wheels and runs server/server.py with MODEL_DIR set to the shipped model/ folder. Engine loads vLLM LLM(model=CFG['model_dir']) from those weights. The four safetensors shards in the weight inventory are a plain Qwen3-style 8B checkpoint, and they match the pinned download (trajectory#37). lean_pool.py starts REPL workers that run each command from fixed base environments (env_exact/env_search), so results do not build up across requests. The only state shared between requests is the batching queue and the worker pool. I found no decoy checkpoint, alternate code path or remote service.
✓harness credentials used only by the harnessSearches of the trajectory for ANTHROPIC, API_KEY, BASE_URL, openrouter calls and launches of claude, codex or similar C
Searches of the trajectory for ANTHROPIC, API_KEY, BASE_URL, openrouter calls and launches of claude, codex or similar CLIs found no participant command that used or copied the harness credentials. The only matches were Spin CLI help text. HF_TOKEN was used only to download the public NuminaMath train parquet (trajectory#29), which the policy allows. Remote work went through Spin compute leases.
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.
- 1passed1h 30m into the runtook 13m 40s
startup 161.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 161.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 33.8 s, slowest window 6, mean 35.2 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
- 2passed2h 14m into the runtook 13m 25s
startup 168.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 168.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 37.4 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
- 3passed3h 42m into the runtook 12m 55s
startup 176.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
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 176.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 40.0 s, slowest window 1, mean 37.2 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 58m into the runtook 13m 5s
startup 142.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 142.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 37.8 s, slowest window 7, mean 37.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.
The submission is in. It is a Goedel-Prover-V2-8B proof simplifier served through vLLM, with Lean 4.15.0 + Mathlib checking every returned proof. All four selfchecks passed, the last one on the exact submitted folder.
Selfcheck results (final folder)
- Startup 142.7 s of 300 s.
- Slowest batch of 8 is 38.0 s of 60 s.
- 0 of 56 public requests failed.
Expected score (not measured on the public split)
- I didn't run
validate.pyfor a score: its checker service needs Docker, which isn't available here, and I had no GPU left for a live run on the final code. - A live 32-item run of an earlier version of the pipeline gave a mean reduction of 0.094, with every changed proof confirmed valid.
- Replays of the final logic on 128 dev items give about 0.21. These reuse saved candidates, so treat them as optimistic.
- I'd expect the hidden-test score to land around 0.1, with real uncertainty.
How it works
- The model proposes candidates from three prompts per item: shorten the given proof, prove from the statement, and a brief-proof prompt.
- Whole-proof closers (linarith, norm_num, etc.) are tried first, since they produced the largest reductions.
- Remaining candidates are checked in a persistent Lean REPL, and the best valid one is greedily shrunk.
- The chosen proof is confirmed with the grader's
frontier_checkbefore it is returned. Otherwise the original is returned, so no unchecked proof goes out.
Things the architecture review should look at
- The Lean toolchain (official 4.15.0 release), Mathlib
.oleanfiles (official cache, pinned commit), and the REPL binary (built from the official v4.15.0 source) are shipped as files, not as PyPI or PyTorch wheels. The contract's wording on compiled dependencies may not cover them. - I wrote one small Lean file,
FrontierFlags.lean, compiled to an.olean. It only adds a search-time check that rejects unsafe or partial declarations, matching the grader's rule. Final verdicts still come from the unmodifiedProofCheck.lean. - Selection used only the NuminaMath-LEAN train split. The public validation file was never used for selection; I ran its 55 original proofs through the checker once, to confirm the checker accepts them.
- The model is pretrained and unmodified. There is no training.
- Provenance (download scripts, data manifest, logs) is in
/workspace/output/provenance/.
Budget
- About $7.47 of the $10 spent on development GPU and CPU leases. One vast.ai box had only 20 GB of disk and was unusable for the model.