Math proof simplification
- Score
- 3.3
- Wallet spend
- $29.44 of $200
- Model cost
- $23.15
- Agent time
- 4h 46m
- Steps
- 281
- Tokens in / out
- 72.5M / 249k
- Self-checks
- 3 passed of 3 used
- Rank at $200 wallet
- 9th of 14
Score
3.3raw metric 0.03253
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.1356
- standard_error
- 0.0056
- proof_checking_seconds
- 94.0141
- preflight_seconds
- 769.9522
- 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 provenanceThe only training corpus is the public AI-MO/NuminaMath-LEAN train split (train-00000-of-00001.parquet). It is declared
The only training corpus is the public AI-MO/NuminaMath-LEAN train split (train-00000-of-00001.parquet). It is declared in data_manifest.json, TRAINING_LOG.md and download_data.sh, which records the exact curl command. The trajectory shows that HF download being run (steps 101-114). training/build_numina.py drops rows with source=='math_test' and opens the public validation file only to exclude statements that match it. training/datagen.py builds the targets with the server's own symbolic search, and training/build_train_data*.py and training/train_lora.py build the SFT data and fine-tune Goedel-Prover-V2-8B with LoRA. The base model was fetched from HF at the declared revision dfd02e6 (trajectory#188 and trajectory#231). The adapter trained on the rented H100 was transferred back, checked by sha256, and merged locally with merge_and_unload into model/ (trajectory#235, trajectory#237, trajectory#239). Public validation rows were used only to evaluate the finished server, never as training data. One minor gap: train_lora.py defaults to 3 epochs, while the log says 4; the epoch count can be set by environment variable, so this does not change the provenance.
✓no proof lookupserver.py builds candidates only from generic tactics, hints taken from the request's own proof, templates, and edits of
server.py builds candidates only from generic tactics, hints taken from the request's own proof, templates, and edits of the submitted proof. Each candidate is checked with the bundled Lean/Mathlib toolchain and re-verified standalone before it is returned. I found no table keyed by statement, no stored proof corpus, no cache, and no network calls. llm_worker.py builds its prompt from the request statement only. The shipped evidence contains no jsonl, pickle or SQLite data files.
✓actual inference pathserve.sh installs the vendored wheels offline (--no-index) and then runs server.py. server.py runs the symbolic Lean-ver
serve.sh installs the vendored wheels offline (--no-index) and then runs server.py. server.py runs the symbolic Lean-verified search and launches llm_worker.py. llm_worker.py calls AutoModelForCausalLM.from_pretrained on ROOT/model, which holds the shipped merged Qwen3 8B weights in 4 safetensors shards; the inventory matches the Goedel-Prover-V2-8B architecture. Every LLM output is verified by Lean before it can be returned. The trajectory shows these same files being uploaded and served during full-stack scoring (trajectory#245, trajectory#246).
✓harness credentials used only by the harnessThe participant used only its own Spin allowance: an openrouter key created with spin CLI (trajectory#46) and spin compu
The participant used only its own Spin allowance: an openrouter key created with spin CLI (trajectory#46) and spin compute for the H100. It used the provided read-only HF_TOKEN only for the public HF downloads. I found no use of Anthropic, OpenRouter or other harness credentials, no harness setup files read, and no extra agent sessions. The shipped server makes no 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.
- 1passed1h 25m into the runtook 7m 56s
startup 4.2 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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 4.2 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 39.2 s, slowest window 2, mean 40.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
- 2passed4h 10m into the runtook 12m 58s
startup 4.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 4.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 40.2 s, slowest window 3, mean 40.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
- 3passed4h 33m into the runtook 11m 55s
startup 3.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 3.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 42.3 s, slowest window 4, mean 42.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